pow_eq_zero_iff' — Mathlib

English

For a nontrivial ring, x^n = 0 iff x = 0 and n ≠ 0.

Русский

Для ненулевого кольца x^n = 0 тогда и только тогда, когда x = 0 и n ≠ 0.

LaTeX

$$$\forall n\, (\mathrm{nilpotence}) \; x^n = 0 \iff (x = 0 \land n \neq 0)$$$

Lean4

/-- A variant of `IsReduced.pow_eq_zero_iff` assuming `R` is not trivial. -/
@[simp]
theorem pow_eq_zero_iff' [MonoidWithZero R] [IsReduced R] [Nontrivial R] {n : ℕ} : x ^ n = 0 ↔ x = 0 ∧ n ≠ 0 := by
  cases n <;> simp

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