mk_zero' — Mathlib

English

For any n with NeZero n, the element ⟨0, pos_of_neZero n⟩ in Fin n equals 0.

Русский

Для любого n с не нулём, элемент ⟨0, pos_of_neZero n⟩ в Fin n равен 0.

LaTeX

$$$(\langle 0, \mathrm{pos\_of\_neZero}(n)\rangle : Fin(n)) = 0$$$

Lean4

/-- `Fin.mk_zero` in `Lean` only applies in `Fin (n + 1)`.
This one instead uses a `NeZero n` typeclass hypothesis.
-/
@[simp]
theorem mk_zero' (n : ℕ) [NeZero n] : (⟨0, pos_of_neZero n⟩ : Fin n) = 0 :=
  rfl

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