Ideal.height_map_quotientMk_span_singleton_add_one
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_height_map_quotientMk_span_singleton_add_one
universe u
open IsLocalRingLean source · statement
theorem _root_.Ideal.height_map_quotientMk_span_singleton_add_one
{R : Type u} [CommRing R] [IsNoetherianRing R] (p : Ideal R) [p.IsPrime] {x : R} (hx : x ∈ p)
(hxmin : ∀ q ∈ minimalPrimes R, q ≤ p → x ∉ q) :
(p.map (Ideal.Quotient.mk (Ideal.span {x}))).height + 1 = p.height