isReduced_iff_pow_one_lt — Mathlib

English

For k > 1, IsReduced R iff every x with x^k = 0 satisfies x = 0.

Русский

Для k > 1, IsReduced R эквивалентно тому, что из x^k = 0 следует x = 0.

LaTeX

$$$\\text{IsReduced }R \\iff \\forall x:\\ x^k = 0 \\rightarrow x = 0\\quad (k>1)$$$

Lean4

theorem isReduced_iff_pow_one_lt [MonoidWithZero R] (k : ℕ) (hk : 1 < k) : IsReduced R ↔ ∀ x : R, x ^ k = 0 → x = 0 :=
  by simp_rw [← zero_isRadical_iff, isRadical_iff_pow_one_lt k hk, zero_dvd_iff]

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