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.

We also prove a lemma about parity of Fin.succAbove i j + Fin.predAbove j i which can be used to prove d ∘ d = 0 for de Rham cohomologies.

theorem Fin.even_succAbove_add_predAbove {n : ℕ} (i : Fin (n + 1)) (j : Fin n) : Even (↑(i.succAbove j) + ↑(j.predAbove i)) ↔ Odd (↑i + ↑j)

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

theorem Fin.odd_of_val {n : ℕ} {k : Fin n} [NeZero 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 : ℕ} {k : Fin n} (hn : Even n) : Even k ↔ Even ↑k

theorem Fin.odd_iff_of_even {n : ℕ} {k : Fin n} [NeZero n] (hn : Even 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 : ℕ} {k : Fin n} [NeZero 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 : ℕ} {k : Fin n} [NeZero n] : Odd k ↔ Even n → Odd ↑k

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

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

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

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

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

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