Ideal.isReduced_quotient_span_singleton_of_forall_mem_associatedPrimes
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_isReduced_quotient_span_singleton_of_forall_mem_associatedPrimes
open IsLocalRingLean source · statement
theorem _root_.Ideal.isReduced_quotient_span_singleton_of_forall_mem_associatedPrimes
{A : Type*} [CommRing A] [IsNoetherianRing A] (x : A)
(h : ∀ (P : Ideal A) [P.IsPrime], P ∈ associatedPrimes A (A ⧸ Ideal.span {x}) →
Ideal.map (algebraMap A (Localization.AtPrime P)) (Ideal.span {x}) =
maximalIdeal (Localization.AtPrime P)) :
IsReduced (A ⧸ Ideal.span {x})