radical_minimalPrimes — Mathlib

English

The radical operation does not change the set of minimal primes: radical(I).minimalPrimes = I.minimalPrimes.

Русский

Операция радикала не изменяет множество минимальных простых: I.radical.minimalPrimes = I.minimalPrimes.

LaTeX

$$$I.\mathrm{radical}.minimalPrimes = I.minimalPrimes$$$

Lean4

@[simp]
theorem radical_minimalPrimes : I.radical.minimalPrimes = I.minimalPrimes :=
  by
  rw [Ideal.minimalPrimes, Ideal.minimalPrimes]
  ext p
  refine ⟨?_, ?_⟩ <;> rintro ⟨⟨a, ha⟩, b⟩
  · refine ⟨⟨a, a.radical_le_iff.1 ha⟩, ?_⟩
    simp only [and_imp] at *
    exact fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.2 h3) h4
  · refine ⟨⟨a, a.radical_le_iff.2 ha⟩, ?_⟩
    simp only [and_imp] at *
    exact fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.1 h3) h4

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