ofInt'_eq — Mathlib

English

For every integer n, ZNum.ofInt' n = n (as a ZNum).

Русский

Для каждого целого числа n: ZNum.ofInt' n = n (как ZNum).

LaTeX

$$$$\forall n \in \mathbb{Z},\ ZNum.ofInt' n = n.$$$$

Lean4

@[simp]
theorem ofInt'_eq : ∀ n : ℤ, ZNum.ofInt' n = n
  | (n : ℕ) => rfl
  | -[n+1] => by
    change Num.toZNumNeg (n + 1 : ℕ) = -(n + 1 : ℕ)
    rw [← neg_inj, neg_neg, Nat.cast_succ, Num.add_one, Num.zneg_toZNumNeg, Num.toZNum_succ, Nat.cast_succ,
      ZNum.add_one]
    rfl

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