isIrreducible_iff_vanishingIdeal_isPrime

English

For any set s, IsIrreducible s iff vanishingIdeal s is prime.

Русский

Для множества s верно: IsIrreducible s эквивално prime-идеал vanishingIdeal s.

LaTeX

$$$\\text{IsIrreducible}(s) \\iff (\\operatorname{vanishingIdeal}(s)).IsPrime$$$

Lean4

theorem isIrreducible_iff_vanishingIdeal_isPrime {s : Set (PrimeSpectrum R)} :
    IsIrreducible s ↔ (vanishingIdeal s).IsPrime := by
  rw [← isIrreducible_iff_closure, ← zeroLocus_vanishingIdeal_eq_closure,
    isIrreducible_zeroLocus_iff_of_radical _ (isRadical_vanishingIdeal s)]

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