minimalPrimes_eq_subsingleton_self

English

If I is prime, then its minimal primes consist only of I itself.

Русский

Если I — простой идеал, то I.minimalPrimes = { I }.

LaTeX

$$$[I\text{ prime}]\ \Rightarrow I.minimalPrimes = \{ I \}$$$

Lean4

theorem minimalPrimes_eq_subsingleton_self [I.IsPrime] : I.minimalPrimes = { I } :=
  by
  ext J
  constructor
  · exact fun H => (H.2 ⟨inferInstance, rfl.le⟩ H.1.2).antisymm H.1.2
  · rintro (rfl : J = I)
    exact ⟨⟨inferInstance, rfl.le⟩, fun _ h _ => h.2⟩

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