Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `IsDedekindDomain`, `IsDedekindRing`, `DimensionLEOne`	3
Theorems `isMaximal`, `toIsDedekindRing`, `toIsDomain`, `toDimensionLEOne`, `toIsIntegralClosure`, `toIsNoetherian`, `primesOver_eq`, `isDedekindDomain`, `eq_bot_of_lt`, `integralClosure`, `isIntegralClosure`, `maximalOfPrime`, `not_lt_lt`, `principal_ideal_ring`, `instIsDedekindDomainOfIsDomainOfIsDedekindRing`, `isDedekindDomain_iff`, `isDedekindRing_iff`	17
Total	20

Ideal.IsPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMaximal` 📖	mathematical	—	`Ideal.IsMaximal` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`Ring.DimensionLEOne.maximalOfPrime`

IsDedekindDomain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toIsDedekindRing` 📖	mathematical	—	`IsDedekindRing`	—	—
`toIsDomain` 📖	mathematical	—	`IsDomain` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	—

IsDedekindRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toDimensionLEOne` 📖	mathematical	—	`Ring.DimensionLEOne`	—	—
`toIsIntegralClosure` 📖	mathematical	—	`IsIntegralClosure` `FractionRing` `CommRing.toCommSemiring` `OreLocalization.instCommRing` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommRing.toCommMonoid` `OreLocalization.instAlgebra` `Algebra.id`	—	—
`toIsNoetherian` 📖	mathematical	—	`IsNoetherian` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule`	—	—

IsLocalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`primesOver_eq` 📖	mathematical	—	`Ideal.primesOver` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Ideal` `Set` `Set.instSingletonSet` `maximalIdeal`	—	`IsDomain.of_faithfulSMul` `IsDedekindDomain.toIsDomain` `Set.eq_singleton_iff_nonempty_unique_mem` `Ideal.exists_maximal_ideal_liesOver_of_isIntegral` `Algebra.IsIntegral.of_finite` `Ideal.IsMaximal.isPrime` `eq_maximalIdeal` `Ideal.IsPrime.isMaximal` `IsDedekindRing.toDimensionLEOne` `IsDedekindDomain.toIsDedekindRing` `Ideal.ne_bot_of_mem_primesOver` `toNontrivial` `FaithfulSMul.to_isTorsionFree` `IsDomain.toNontrivial` `IsDomain.toIsCancelMulZero`

IsPrincipalIdealRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isDedekindDomain` 📖	mathematical	—	`IsDedekindDomain`	—	`PrincipalIdealRing.isNoetherianRing` `Ring.DimensionLEOne.principal_ideal_ring` `UniqueFactorizationMonoid.instIsIntegrallyClosed` `PrincipalIdealRing.to_uniqueFactorizationMonoid`

Ring

Definitions

Name	Category	Theorems
`DimensionLEOne` 📖	CompData	9 math math: `IsDedekindDomainDvr.ring_dimensionLEOne`, `IsDedekindDomainInv.dimensionLEOne`, `DimensionLEOne.principal_ideal_ring`, `DimensionLEOne.isIntegralClosure`, `DimensionLEOne.integralClosure`, `DimensionLEOne.localization`, `isDedekindRing_iff`, `IsDedekindRing.toDimensionLEOne`, `isDedekindDomain_iff`

Ring.DimensionLEOne

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_bot_of_lt` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Bot.bot` `Submodule.instBot`	—	`by_contra` `not_lt_lt` `Ne.bot_lt`
`integralClosure` 📖	mathematical	—	`Ring.DimensionLEOne` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `integralClosure` `Subalgebra.toCommRing`	—	`isIntegralClosure` `instIsDomainSubtypeMemSubalgebraIntegralClosure` `IsScalarTower.subalgebra'` `IsScalarTower.right` `integralClosure.isIntegralClosure`
`isIntegralClosure` 📖	mathematical	—	`Ring.DimensionLEOne`	—	`Ideal.IsIntegralClosure.isMaximal_of_isMaximal_comap` `Ideal.IsPrime.isMaximal` `RingHom.instRingHomClass` `Ideal.IsPrime.under` `Ideal.IsIntegralClosure.comap_ne_bot`
`maximalOfPrime` 📖	mathematical	—	`Ideal.IsMaximal` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	—
`not_lt_lt` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`LT.lt.ne` `Ideal.IsMaximal.eq_of_le` `Ideal.IsPrime.isMaximal` `LT.lt.ne'` `LE.le.trans_lt` `bot_le` `Ideal.IsPrime.ne_top` `LT.lt.le`
`principal_ideal_ring` 📖	mathematical	—	`Ring.DimensionLEOne`	—	`IsPrime.to_maximal_ideal`

(root)

Definitions

Name	Category	Theorems
`IsDedekindDomain` 📖	CompData	19 math math: `NumberField.RingOfIntegers.instIsDedekindDomainWithVal`, `integralClosure.isDedekindDomain`, `Localization.AtPrime.isDedekindDomain`, `IsPrincipalIdealRing.isDedekindDomain`, `Ring.instIsDedekindDomainNormalClosure`, `IsDedekindDomainDvr.isDedekindDomain`, `isDedekindDomain_iff_isDedekindDomainInv`, `NumberField.RingOfIntegers.instIsDedekindDomain`, `tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain`, `IsLocalization.isDedekindDomain`, `FunctionField.ringOfIntegers.instIsDedekindDomainSubtypeMemSubalgebraPolynomialOfIsSeparableRatFunc`, `IsDiscreteValuationRing.TFAE`, `IsLocalization.AtPrime.isDedekindDomain`, `instIsDedekindDomainOfIsDomainOfIsDedekindRing`, `integralClosure.isDedekindDomain_fractionRing`, `isDedekindDomain_iff`, `instIsDedekindDomainLocalizationAlgebraMapSubmonoidPrimeCompl`, `IsDedekindDomainInv.isDedekindDomain`, `IsIntegralClosure.isDedekindDomain`
`IsDedekindRing` 📖	CompData	2 math math: `IsDedekindDomain.toIsDedekindRing`, `isDedekindRing_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsDedekindDomainOfIsDomainOfIsDedekindRing` 📖	mathematical	—	`IsDedekindDomain`	—	—
`isDedekindDomain_iff` 📖	mathematical	—	`IsDedekindDomain` `IsDomain` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IsNoetherianRing` `Ring.DimensionLEOne` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	`IsDedekindDomain.toIsDomain` `IsDedekindRing.toIsNoetherian` `IsDedekindDomain.toIsDedekindRing` `IsDedekindRing.toDimensionLEOne` `isIntegrallyClosed_iff` `IsDedekindRing.toIsIntegralClosure`
`isDedekindRing_iff` 📖	mathematical	—	`IsDedekindRing` `IsNoetherianRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.DimensionLEOne` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	`IsDedekindRing.toIsNoetherian` `IsDedekindRing.toDimensionLEOne` `isIntegrallyClosed_iff` `IsDedekindRing.toIsIntegralClosure`

---

← Back to Index