mul_neg_one_pow_eq_zero_iff — Mathlib

English

In a ring with distributive negation, for all a ∈ R and n ∈ ℕ, a · (-1)^n = 0 iff a = 0.

Русский

В кольце с распределимым отрицанием для любого a и n верно: a · (-1)^n = 0 тогда и только тогда, когда a = 0.

LaTeX

$$$ a \\cdot (-1)^n = 0 \\iff a = 0 $$$

Lean4

@[simp]
theorem mul_neg_one_pow_eq_zero_iff : a * (-1) ^ n = 0 ↔ a = 0 := by obtain h | h := neg_one_pow_eq_or R n <;> simp [h]

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