Module

Localization_AtPrime_isDiscreteValuationRing_of_height_eq_one.lean

Nyll.AlgebraicCurves.Valuations.Localization_AtPrime_isDiscreteValuationRing_of_height_eq_one

1 declaration indexed from sourceView source ↗

Module documentation

Localization At Prime is Discrete Valuation Ring of height eq one

Imports26

Mathlib.Algebra.Algebra.Defs
Mathlib.Algebra.Group.Hom.Defs
Mathlib.Algebra.Module.Submodule.Lattice
Mathlib.Algebra.NeZero
Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Mathlib.Algebra.Ring.Defs
Mathlib.Data.List.TFAE
Mathlib.Data.Nat.Cast.Defs
Mathlib.Order.Defs.PartialOrder
Mathlib.RingTheory.DiscreteValuationRing.Basic
Mathlib.RingTheory.DiscreteValuationRing.TFAE
Mathlib.RingTheory.Ideal.Defs
Mathlib.RingTheory.Ideal.Height
Mathlib.RingTheory.Ideal.Lattice
Mathlib.RingTheory.Ideal.Maps
Mathlib.RingTheory.Ideal.Maximal
Mathlib.RingTheory.Ideal.Operations
Mathlib.RingTheory.Ideal.Prime
Mathlib.RingTheory.Ideal.Span
Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Mathlib.RingTheory.KrullDimension.Basic
Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Mathlib.RingTheory.Localization.AtPrime.Basic
Mathlib.RingTheory.Localization.Defs
Mathlib.RingTheory.Localization.Submodule
Mathlib.RingTheory.Noetherian.Defs

Imported by2

theorem

isDiscreteValuationRing_of_height_eq_one

L51 ↗

Localization.AtPrime.isDiscreteValuationRing_of_height_eq_one

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace Localization_AtPrime_isDiscreteValuationRing_of_height_eq_one
open IsLocalRing

Lean source · statement

theorem _root_.Localization.AtPrime.isDiscreteValuationRing_of_height_eq_one
    {R : Type*} [CommRing R] [IsDomain R] [IsNoetherianRing R] [IsIntegrallyClosed R]
    (p : Ideal R) [p.IsPrime] (hp : p.height = 1) :
    IsDiscreteValuationRing (Localization.AtPrime p)

Module documentation

Localization At Prime is Discrete Valuation Ring of height eq one

Declarations

isDiscreteValuationRing_of_height_eq_one