isPrime_radical — Mathlib

English

The radical of a primary ideal is prime.

Русский

Радикал примарного идеала являетсяprime.

LaTeX

$$$\\sqrt{I} \\text{ is prime if } I \\text{ is primary}.$$$

Lean4

theorem isPrime_radical {I : Ideal R} (hi : I.IsPrimary) : IsPrime (radical I) :=
  ⟨mt radical_eq_top.1 hi.1, fun {x y} ⟨m, hxy⟩ =>
    by
    rw [mul_pow] at hxy; rcases (isPrimary_iff.mp hi).2 hxy with h | h
    · exact Or.inl ⟨m, h⟩
    · exact Or.inr (mem_radical_of_pow_mem h)⟩

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