IsIntegrallyClosed.isReduced_quotient_span_singleton_of_forall_mem_minimalPrimes
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsIntegrallyClosed_isReduced_quotient_span_singleton_of_forall_mem_minimalPrimesLean source · statement
theorem _root_.IsIntegrallyClosed.isReduced_quotient_span_singleton_of_forall_mem_minimalPrimes
{A : Type*} [CommRing A] [IsDomain A] [IsNoetherianRing A] [IsIntegrallyClosed A]
{x : A} (hx : x ≠ 0)
(h : ∀ (P : Ideal A) [P.IsPrime], P ∈ (Ideal.span {x}).minimalPrimes →
Ideal.map (algebraMap A (Localization.AtPrime P)) (Ideal.span {x}) =
IsLocalRing.maximalIdeal (Localization.AtPrime P)) :
IsReduced (A ⧸ Ideal.span {x})