English
In Fin n, k is odd exactly when either n is odd or k.val is odd.
Русский
В Fin n элемент нечетен тогда и только тогда, когда либо n нечетно, либо k.val нечетно.
LaTeX
$$$\mathrm{Odd}(k) \iff (\mathrm{Odd}(n) \lor \mathrm{Odd}(k.\mathrm{val})).$$$
Lean4
/-- In `Fin n`, all elements are odd for odd `n`,
otherwise an element is odd iff its `Fin.val` value is odd. -/
theorem odd_iff [NeZero n] : Odd k ↔ Odd n ∨ Odd k.val :=
by
refine ⟨fun hk ↦ ?_, or_imp.mpr ⟨(odd_of_odd · k), odd_of_val⟩⟩
rw [← Nat.not_even_iff_odd, ← imp_iff_not_or]
exact fun hn ↦ (odd_iff_of_even hn).mp hk