sInf_minimalPrimes — Mathlib

English

For any ring, the radical of I has the same minimal primes as I itself.

Русский

Для любого кольца радикал I и минимальные-primes I совпадают по набору.

LaTeX

$$$I.radical.minimalPrimes = I.minimalPrimes$$$

Lean4

@[simp]
theorem sInf_minimalPrimes : sInf I.minimalPrimes = I.radical :=
  by
  rw [I.radical_eq_sInf]
  apply le_antisymm
  · intro x hx
    rw [Ideal.mem_sInf] at hx ⊢
    rintro J ⟨e, hJ⟩
    obtain ⟨p, hp, hp'⟩ := Ideal.exists_minimalPrimes_le e
    exact hp' (hx hp)
  · apply sInf_le_sInf _
    intro I hI
    exact hI.1.symm

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