Parity in Fin n

In this file we prove that an element k : Fin n is even in Fin n iff n is odd or Fin.val k is even.

theorem Fin.even_of_val {n : ℕ} {k : Fin n} (h : Even ↑k) : Even k

theorem Fin.odd_of_val {n : ℕ} [NeZero n] {k : Fin n} (h : Odd ↑k) : Odd k

theorem Fin.even_of_odd {n : ℕ} (hn : Odd n) (k : Fin n) : Even k

theorem Fin.odd_of_odd {n : ℕ} [NeZero n] (hn : Odd n) (k : Fin n) : Odd k

theorem Fin.even_iff_of_even {n : ℕ} (hn : Even n) {k : Fin n} : Even k ↔ Even ↑k

theorem Fin.odd_iff_of_even {n : ℕ} [NeZero n] (hn : Even n) {k : Fin n} : Odd k ↔ Odd ↑k

theorem Fin.even_iff {n : ℕ} {k : Fin n} : Even k ↔ Odd n ∨ Even ↑k

In Fin n, all elements are even for odd n, otherwise an element is even iff its Fin.val value is even.

theorem Fin.even_iff_imp {n : ℕ} {k : Fin n} : Even k ↔ Even n → Even ↑k

theorem Fin.odd_iff {n : ℕ} [NeZero n] {k : Fin n} : Odd k ↔ Odd n ∨ Odd ↑k

In Fin n, all elements are odd for odd n, otherwise an element is odd iff its Fin.val value is odd.

theorem Fin.odd_iff_imp {n : ℕ} [NeZero n] {k : Fin n} : Odd k ↔ Even n → Odd ↑k

theorem Fin.even_iff_mod_of_even {n : ℕ} (hn : Even n) {k : Fin n} : Even k ↔ ↑k % 2 = 0

theorem Fin.odd_iff_mod_of_even {n : ℕ} [NeZero n] (hn : Even n) {k : Fin n} : Odd k ↔ ↑k % 2 = 1

theorem Fin.not_odd_iff_even_of_even {n : ℕ} [NeZero n] (hn : Even n) {k : Fin n} : ¬Odd k ↔ Even k

theorem Fin.not_even_iff_odd_of_even {n : ℕ} [NeZero n] (hn : Even n) {k : Fin n} : ¬Even k ↔ Odd k

theorem Fin.odd_add_one_iff_even {n : ℕ} [NeZero n] {k : Fin n} : Odd (k + 1) ↔ Even k

theorem Fin.even_add_one_iff_odd {n : ℕ} [NeZero n] {k : Fin n} : Even (k + 1) ↔ Odd k