cast_neg — Mathlib

English

The cast of a negated integer equals the negation of its cast for any AddGroupWithOne.

Русский

Образ отображения отрицательного целого числа равен отрицательному образу его отображения в любой группе с единицей.

LaTeX

$$$\mathrm{Int}.cast\_neg : \text{(for all integers } n) \ ((-n) : R) = - (n : R)$$$

Lean4

@[simp, norm_cast]
theorem cast_neg : ∀ n, ((-n : ℤ) : R) = -n
  | (0 : ℕ) => by simp
  | (n + 1 : ℕ) => by rw [cast_natCast, neg_ofNat_succ]; simp
  | -[n+1] => by rw [Int.neg_negSucc, cast_natCast]; simp

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