cast_eq_zero — Mathlib

English

If k = l and k,l ≠ 0, then for any x ∈ Fin(k), Fin.cast h x = 0 iff x = 0; casting preserves zero exactly at zero.

Русский

Пусть k = l и k,l ≠ 0; для любого x ∈ Fin(k) выполняется Fin.cast h x = 0 тогда и только тогда, когда x = 0; кастинг сохраняет ноль только для нуля.

LaTeX

$$$$\forall k,l:\\mathbb{N}, [\mathrm{NeZero}\ k][\mathrm NeZero\ l](h:\,k=l)\;\forall x:\\mathrm{Fin}(k),\; \mathrm{Fin.cast}(h\,x)=0 \iff x=0.$$$$

Lean4

@[simp]
theorem cast_eq_zero {k l : ℕ} [NeZero k] [NeZero l] (h : k = l) (x : Fin k) : Fin.cast h x = 0 ↔ x = 0 := by
  simp [← val_eq_zero_iff]

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