of_to_int' — Mathlib

English

For every z ∈ ZNum, applying ofInt' to the image of z (under the cast) yields z.

Русский

Для каждого z ∈ ZNum применение ofInt' к образу z возвращает z.

LaTeX

$$$$\forall n \in ZNum,\ ZNum.ofInt' (n.cast) = n.$$$$

Lean4

theorem of_to_int' : ∀ n : ZNum, ZNum.ofInt' n = n
  | 0 => by
    dsimp [ofInt', cast_zero]
    simp only [Num.ofNat'_zero, Num.toZNum]
  | pos a => by rw [cast_pos, ← PosNum.cast_to_nat, ← Num.ofInt'_toZNum, PosNum.of_to_nat]; rfl
  | neg a => by rw [cast_neg, ofInt'_neg, ← PosNum.cast_to_nat, ← Num.ofInt'_toZNum, PosNum.of_to_nat]; rfl

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