cast_eq_neg_cast — Mathlib

English

Let R be a ring with an order, and m,n be natural numbers. The only way to have the natural cast of m equal the additive inverse of n is when m and n are both zero.

Русский

Пусть R — кольцо с порядком, m,n ∈ ℕ. Еденица m, отображённая в R, равна противоположному числу n тогда и только тогда, когда m = 0 и n = 0.

LaTeX

$$$ (m : R) = -n \iff m = 0 \land n = 0 $$$

Lean4

@[simp, norm_cast]
theorem cast_eq_neg_cast : (m : R) = -n ↔ m = 0 ∧ n = 0 := by simp [eq_neg_iff_add_eq_zero, ← cast_add]

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