English
Let R be a division ring. For every natural number n, the image of −n in R equals the additive inverse of the image of n in R.
Русский
Пусть R — кольцо деления. Для любого натурального числа n образ −n в R равен противолежащему образу n в R.
LaTeX
$$$ \forall R\,[DivisionRing\ R],\ \forall n \in \mathbb{N},\ ((-n:\mathbb{Z}) : R) = -(n : R).$$$
Lean4
/-- Auxiliary lemma for norm_cast to move the cast `-↑n` upwards to `↑-↑n`.
(The restriction to `DivisionRing` is necessary, otherwise this would also apply in the case where
`R = ℤ` and cause nontermination.)
-/
@[norm_cast]
theorem cast_neg_natCast {R} [DivisionRing R] (n : ℕ) : ((-n : ℤ) : R) = -n := by simp
