odd_iff — Mathlib

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

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