even_of_odd — Mathlib

English

If n is odd, every element of Fin n is even.

Русский

Если n нечетно, то каждый элемент Fin n четен.

LaTeX

$$$\forall n:\mathbb{N},\; \mathrm{Odd}(n)\Rightarrow \forall k:\mathrm{Fin}(n),\; \mathrm{Even}(k).$$$

Lean4

theorem even_of_odd (hn : Odd n) (k : Fin n) : Even k :=
  by
  have : NeZero n := ⟨k.pos.ne'⟩
  rcases k.val.even_or_odd with hk | hk
  · exact even_of_val hk
  · simpa using (hk.add_odd hn).natCast (α := Fin n)

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