Dvr

📁 Source: Mathlib/RingTheory/DedekindDomain/Dvr.lean

Statistics

Metric	Count
Definitions IsDedekindDomainDvr	1
Theorems isDedekindDomainDvr, isDedekindDomain, isIntegrallyClosed, is_dvr_at_nonzero_prime, ring_dimensionLEOne, toIsNoetherian, isDedekindDomain, isDiscreteValuationRing_of_dedekind_domain, not_isField, isDedekindDomain, isDedekindDomain, localization	12
Total	13

IsDedekindDomain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isDedekindDomainDvr 📖	mathematical	—	IsDedekindDomainDvr	—	IsDedekindRing.toIsNoetherian toIsDedekindRing IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain IsLocalization.isDomain_of_local_atPrime Localization.isLocalization

IsDedekindDomainDvr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isDedekindDomain 📖	mathematical	—	IsDedekindDomain	—	toIsNoetherian ring_dimensionLEOne isIntegrallyClosed
isIntegrallyClosed 📖	mathematical	—	IsIntegrallyClosed	—	IsIntegrallyClosed.of_localization_maximal Ideal.IsMaximal.isPrime' IsLocalization.isDomain_of_local_atPrime IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime is_dvr_at_nonzero_prime Ideal.IsMaximal.isPrime IsDedekindRing.toIsIntegralClosure IsDedekindDomain.toIsDedekindRing IsPrincipalIdealRing.isDedekindDomain
is_dvr_at_nonzero_prime 📖	mathematical	—	IsDiscreteValuationRing Localization.AtPrime CommRing.toCommSemiring OreLocalization.instCommRing Ideal.primeCompl CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid IsLocalization.isDomain_of_local_atPrime	—	—
ring_dimensionLEOne 📖	mathematical	—	Ring.DimensionLEOne	—	Ideal.exists_le_maximal Ideal.IsPrime.ne_top Ideal.IsMaximal.isPrime' Localization.isLocalization LE.le.disjoint_compl_left Ideal.IsMaximal.isPrime Set.disjoint_left IsLocalization.injective Ideal.primeCompl_le_nonZeroDivisors IsDomain.to_noZeroDivisors Ideal.map_eq_bot_iff_of_injective RingHom.instRingHomClass ne_bot_of_le_ne_bot IsLocalization.isDomain_of_local_atPrime IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime is_dvr_at_nonzero_prime OrderIso.injective ExistsUnique.unique
toIsNoetherian 📖	mathematical	—	IsNoetherian CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule	—	—

IsLocalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isDedekindDomain 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Semiring.toMonoidWithZero	IsDedekindDomain	—	IsDomain.toNontrivial IsDomain.to_noZeroDivisors IsFractionRing.to_map_eq_zero_iff Localization.isLocalization nonZeroDivisors.ne_zero isDedekindDomain_iff IsFractionRing.isFractionRing_of_isDomain_of_isLocalization IsScalarTower.of_algebraMap_eq lift_eq isNoetherianRing IsDedekindRing.toIsNoetherian IsDedekindDomain.toIsDedekindRing Ring.DimensionLEOne.localization IsDedekindRing.toDimensionLEOne IsIntegral.exists_multiple_integral_of_isLocalization isIntegrallyClosed_iff IsDedekindRing.toIsIntegralClosure lift_mk'_spec Algebra.smul_def

IsLocalization.AtPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isDedekindDomain 📖	mathematical	—	IsDedekindDomain	—	IsLocalization.isDedekindDomain Ideal.primeCompl_le_nonZeroDivisors IsDomain.to_noZeroDivisors
isDiscreteValuationRing_of_dedekind_domain 📖	mathematical	—	IsDiscreteValuationRing	—	not_isField List.TFAE.out isLocalRing IsScalarTower.right IsDiscreteValuationRing.TFAE IsLocalization.isNoetherianRing IsDedekindRing.toIsNoetherian IsDedekindDomain.toIsDedekindRing isDedekindDomain
not_isField 📖	mathematical	—	IsField CommSemiring.toSemiring CommRing.toCommSemiring	—	Submodule.ne_bot_iff Ideal.IsMaximal.ne_top isLocalRing IsLocalRing.maximalIdeal.isMaximal Ideal.eq_top_of_isUnit_mem to_map_mem_maximal_iff isUnit_iff_ne_zero map_ne_zero_iff MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsLocalization.injective Ideal.primeCompl_le_nonZeroDivisors IsDomain.to_noZeroDivisors

Localization.AtPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isDedekindDomain 📖	mathematical	—	IsDedekindDomain Localization.AtPrime CommRing.toCommSemiring OreLocalization.instCommRing Ideal.primeCompl CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid	—	IsLocalization.AtPrime.isDedekindDomain IsLocalization.isDomain_of_local_atPrime Localization.isLocalization

Ring.DimensionLEOne

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
localization 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Semiring.toMonoidWithZero	Ring.DimensionLEOne	—	Ideal.isMaximal_def Ideal.IsPrime.ne_top Ideal.maximal_of_no_maximal Ideal.IsMaximal.isPrime RingHom.instRingHomClass OrderIso.lt_iff_lt not_lt_lt IsLocalization.bot_lt_comap_prime

(root)

Definitions

Name	Category	Theorems
IsDedekindDomainDvr 📖	CompData	1 math math: IsDedekindDomain.isDedekindDomainDvr

---

← Back to Index