ofInt'_neg — Mathlib

English

For every integer n, applying ofInt' to -n yields the negation of ofInt' n.

Русский

Для всякого целого числа n применение ofInt' к -n дает - ofInt' n.

LaTeX

$$$$\forall n \in \mathbb{Z},\ ofInt'(-n) = -\,ofInt'(n).$$$$

Lean4

theorem ofInt'_neg : ∀ n : ℤ, ofInt' (-n) = -ofInt' n
  | -[n+1] => show ofInt' (n + 1 : ℕ) = _ by simp only [ofInt', Num.zneg_toZNumNeg]
  | 0 => show Num.toZNum (Num.ofNat' 0) = -Num.toZNum (Num.ofNat' 0) by rw [Num.ofNat'_zero]; rfl
  | (n + 1 : ℕ) => show Num.toZNumNeg _ = -Num.toZNum _ by rw [Num.zneg_toZNum]

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