Theorems · Theorem · commutative algebra

IsLocalization.isDedekindDomain

∀ (A : Type u_1) [inst : CommRing A] [IsDomain A] [IsDedekindDomain A] {M : Submonoid A},
  M ≤ nonZeroDivisors A →
    ∀ (Aₘ : Type u_2) [inst_3 : CommRing Aₘ] [IsDomain Aₘ] [inst_5 : Algebra A Aₘ] [IsLocalization M Aₘ],
      IsDedekindDomain Aₘ

The localization of a Dedekind domain is a Dedekind domain.

Defined in: Mathlib.RingTheory.DedekindDomain.Dvr
Cited by: 1 results in Mathlib
Foundations: Depth 119 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing IsDomain IsDedekindDomain CommRing IsDomain Algebra IsLocalization

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites30

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
CommRingstatement and proof · cited by 17,173
Algebrastatement and proof · cited by 11,388
Algebra.algebraMapproof · cited by 4,706
IsScalarTowerproof · cited by 3,896
Submonoidstatement and proof · cited by 3,086
IsDomainstatement and proof · cited by 2,196
IsUnitproof · cited by 1,602
nonZeroDivisorsstatement and proof · cited by 895
IsFractionRingproof · cited by 738
IsDedekindDomainstatement and proof · cited by 668
IsLocalizationstatement and proof · cited by 636

Cited by1

Results whose statement or proof uses this declaration.

IsLocalization.AtPrime.isDedekindDomainproof · cited by 1