odd_of_val — Mathlib

English

If k.val is odd, then k is odd (provided the index range is nontrivial).

Русский

Если k.val нечетно, тогда k нечетно (при условии ненулевого диапазона).

LaTeX

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

Lean4

theorem odd_of_val [NeZero n] (h : Odd k.val) : Odd k :=
  by
  rw [← Fin.cast_val_eq_self k]
  exact h.natCast

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