minimalPrimes_eq_subsingleton — Mathlib

English

If I is primary, then its minimal primes are exactly the radical of I.

Русский

Если I — первичный идеал, то его минимальные primes равны единственному элементу {√I}.

LaTeX

$$$I\text{ is primary }\Rightarrow I.minimalPrimes = \{ I.radical \}$$$

Lean4

theorem minimalPrimes_eq_subsingleton (hI : I.IsPrimary) : I.minimalPrimes = { I.radical } :=
  by
  ext J
  constructor
  ·
    exact fun H =>
      let e := H.1.1.radical_le_iff.mpr H.1.2
      (H.2 ⟨Ideal.isPrime_radical hI, Ideal.le_radical⟩ e).antisymm e
  · rintro (rfl : J = I.radical)
    exact ⟨⟨Ideal.isPrime_radical hI, Ideal.le_radical⟩, fun _ H _ => H.1.radical_le_iff.mpr H.2⟩

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