Dedekind

📁 Source: Mathlib/RingTheory/Unramified/Dedekind.lean

Statistics

Metric	Count
Definitions	0
Theorems of_formallyUnramified, of_formallyUnramified	2
Total	2

isDedekindDomain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_formallyUnramified 📖	mathematical	—	IsDedekindDomain	—	isDedekindDomainDvr.of_formallyUnramified IsDedekindDomainDvr.isDedekindDomain

isDedekindDomainDvr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_formallyUnramified 📖	mathematical	—	IsDedekindDomainDvr	—	IsNoetherianRing.of_finite IsScalarTower.right IsDedekindDomainDvr.toIsNoetherian IsDedekindDomain.toIsDomain IsDedekindDomain.isDedekindDomainDvr Localization.AtPrime.isLocalRing Ideal.IsPrime.isMaximal IsDedekindDomainDvr.ring_dimensionLEOne Ideal.IsPrime.under Ideal.under_ne_bot Algebra.IsIntegral.of_finite IsDomain.toNontrivial IsArtinianRing.of_finite isArtinian_of_fg_of_artinian' DivisionRing.instIsArtinianRing Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self Module.IsNoetherian.finite QuotientMapQuotient.isNoetherian isNoetherian_of_isNoetherianRing_of_finite Module.Free.of_divisionRing Ideal.IsRadical.radical Algebra.FormallyUnramified.isRadical_map_isMaximal Algebra.EssFiniteType.of_finiteType Module.Finite.finiteType IsLocalization.map_radical Localization.isLocalization IsLocalization.AtPrime.radical_map_of_mem_minimalPrimes Ideal.instIsTwoSided_1 RingHom.instRingHomClass Ideal.minimalPrimes_eq_comap IsArtinianRing.mem_minimalPrimes Ideal.Quotient.instIsPrimeQuotientMapRingHomAlgebraMapMkOfLiesOver Ideal.over_under bot_le Ideal.map_comap_le Localization.AtPrime.map_eq_maximalIdeal Ideal.map_map IsScalarTower.algebraMap_eq OreLocalization.instIsScalarTower Localization.AtPrime.instIsScalarTower IsScalarTower.left instIsPrincipalMapRingHom IsPrincipalIdealRing.principal IsDedekindDomain.isPrincipalIdealRing Localization.AtPrime.isDedekindDomain IsLocalization.isDomain_of_local_atPrime List.TFAE.out IsDiscreteValuationRing.TFAE IsLocalization.instIsNoetherianRingLocalization IsLocalization.AtPrime.not_isField

---

← Back to Index