even_of_val — Mathlib

English

If the underlying value of an element of Fin n is even, then the Fin element itself is even.

Русский

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

LaTeX

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

Lean4

theorem even_of_val (h : Even k.val) : Even k :=
  by
  have : NeZero n := ⟨k.pos.ne'⟩
  rw [← Fin.cast_val_eq_self k]
  exact h.natCast

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