Module

IsIntegrallyClosed_height_eq_one_of_mem_associatedPrimes.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsIntegrallyClosed_height_eq_one_of_mem_associatedPrimes

1 declaration indexed from sourceView source ↗

Module documentation

Is Integrally Closed height eq one of mem associated Primes

Imports2

Imported by4

theorem

height_eq_one_of_mem_associatedPrimes

L26 ↗

IsIntegrallyClosed.height_eq_one_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_height_eq_one_of_mem_associatedPrimes

Lean source · statement

theorem _root_.IsIntegrallyClosed.height_eq_one_of_mem_associatedPrimes
    {B : Type*} [CommRing B] [IsDomain B] [IsNoetherianRing B] [IsIntegrallyClosed B]
    {x : B} (hx : x ≠ 0) (P : Ideal B) [P.IsPrime]
    (hP : P ∈ associatedPrimes B (B ⧸ Ideal.span {x})) : P.height = 1

Module documentation

Is Integrally Closed height eq one of mem associated Primes

Declarations

height_eq_one_of_mem_associatedPrimes