Structures · Algebra
IsDedekindDomain
A Dedekind domain is an integral domain that is Noetherian, integrally closed, and
has Krull dimension at most one.
This is definition 3.2 of [Neukirch1992].
This is exactly IsDedekindRing plus the IsDomain hypothesis.
The integral closure condition is independent of the choice of field of fractions:
use isDedekindDomain_iff to prove IsDedekindDomain for a given fraction_map.
This is the default implementation, but there are equivalent definitions,
IsDedekindDomainDvr and IsDedekindDomainInv.
- Defined in
- Mathlib.RingTheory.DedekindDomain.Basic
- Shape
- One type argument
Extends2
Extended by0
Nothing extends this class yet.
Concrete types that are instances5
- Localization
- NumberField.RingOfIntegers
- Ring.NormalClosure
- Localization.AtPrime
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by812
- IsDedekindDomain.HeightOneSpectrum.valuation
- Ideal.absNorm
- IsDedekindDomain.HeightOneSpectrum.intValuation
- differentIdeal
- Ideal.dvd_iff_le
- IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion
- FractionalIdeal.count
- NumberField.FinitePlace.embedding
- Ideal.relNorm
- IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap
- ClassGroup.mk0
- IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers
- NumberField.HeightOneSpectrum.adicAbv
- FractionalIdeal.absNorm
- Ideal.absNorm_span_singleton
- NumberField.HeightOneSpectrum.absNorm_ne_zero
- Ideal.isPrime_of_prime
- IsDedekindDomain.HeightOneSpectrum.maxPowDividing
- Ideal.prime_of_isPrime
- IsDedekindDomain.HeightOneSpectrum.irreducible
- FractionalIdeal.mk0
- IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg
- IsDedekindDomain.HeightOneSpectrum.associates_irreducible
- IsDedekindDomain.HeightOneSpectrum.intAdicAbv
- IsDedekindDomain.primesOverFinset
- IsDedekindDomain.HeightOneSpectrum.valuation_le_one
- IsDedekindDomain.idealFactorsEquivOfQuotEquiv
- IsDedekindDomain.HeightOneSpectrum.intValuationDef
- IsDedekindDomain.FiniteAdeleRing
- IsDedekindDomain.HeightOneSpectrum.intValuation_le_one
- Set.integer
- coeIdeal_differentIdeal
- NumberField.HeightOneSpectrum.one_lt_absNorm_nnreal
- KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk
- IsDedekindDomain.HeightOneSpectrum.prime
- Ideal.finite_factors
- IsDedekindDomain.idealFactorsFunOfQuotHom
- Ideal.hasFiniteMulSupport
- IsIntegralClosure.isDedekindDomain
- FractionalIdeal.coe_dual_one
- IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv
- Rat.HeightOneSpectrum.primesEquiv
- FractionalIdeal.divMod
- NumberField.FinitePlace.norm_embedding
- Ideal.finprod_heightOneSpectrum_factorization
- Ideal.IsDedekindDomain.ramificationIdx'_ne_zero_of_liesOver
- IsDedekindDomain.HeightOneSpectrum.adicAbv
- Ideal.prime_iff_isPrime
- Ideal.absNorm_dvd_absNorm_of_le
- NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv