Ideal.height_eq_one_of_isDiscreteValuationRing_localization_atPrime
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace Ideal_height_eq_one_of_isDiscreteValuationRing_localization_atPrimeLean source · statement
theorem _root_.Ideal.height_eq_one_of_isDiscreteValuationRing_localization_atPrime {R : Type*}
[CommRing R] [IsDomain R] (p : Ideal R) [p.IsPrime]
(h : IsDiscreteValuationRing (Localization.AtPrime p)) : p.height = 1