even_iff — Mathlib

English

In Fin n, k is even exactly when either n is odd or k.val is even.

Русский

В Fin n элемент четный тогда и только тогда, когда либо n нечетно, либо k.val четно.

LaTeX

$$$\mathrm{Even}(k) \iff (\mathrm{Odd}(n) \lor \mathrm{Even}(k.\mathrm{val})).$$$

Lean4

/-- In `Fin n`, all elements are even for odd `n`,
otherwise an element is even iff its `Fin.val` value is even. -/
theorem even_iff : Even k ↔ (Odd n ∨ Even k.val) :=
  by
  refine ⟨fun hk ↦ ?_, or_imp.mpr ⟨(even_of_odd · k), even_of_val⟩⟩
  rw [← Nat.not_even_iff_odd, ← imp_iff_not_or]
  exact fun hn ↦ (even_iff_of_even hn).mp hk

Похожие утверждения