toZ_of_eq — Mathlib

English

Let i0 be a fixed element. The signed distance from i0 to i0 is 0; equivalently, the value of toZ at (i0, i0) is 0.

Русский

Пусть i0 — фиксированный элемент. Расстояние по знаку от i0 к i0 равно 0; то есть toZ i0 i0 = 0.

LaTeX

$$$toZ(i_0,i_0)=0$$$

Lean4

@[simp]
theorem toZ_of_eq : toZ i0 i0 = 0 := by
  rw [toZ_of_ge le_rfl]
  norm_cast
  refine le_antisymm (Nat.find_le ?_) (zero_le _)
  rw [Function.iterate_zero, id]

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