IsIntegrallyClosed.mem_minimalPrimes_of_mem_associatedPrimes
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsIntegrallyClosed_mem_minimalPrimes_of_mem_associatedPrimesLean source · statement
theorem _root_.IsIntegrallyClosed.mem_minimalPrimes_of_mem_associatedPrimes
{A : Type*} [CommRing A] [IsDomain A] [IsNoetherianRing A] [IsIntegrallyClosed A]
{x : A} (hx : x ≠ 0) (P : Ideal A) [P.IsPrime]
(hP : P ∈ associatedPrimes A (A ⧸ Ideal.span {x})) : P ∈ (Ideal.span {x}).minimalPrimes