odd_of_odd — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem odd_of_odd [NeZero n] (hn : Odd n) (k : Fin n) : Odd k :=
  by
  rcases k.val.even_or_odd with hk | hk
  · simpa using (Even.add_odd hk hn).natCast (R := Fin n)
  · exact odd_of_val hk

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