LocalRing

Statistics

Metric	Count
Definitions	0
Theorems `ringKrullDim_eq_one_iff_of_isLocalRing_isDomain`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`ringKrullDim_eq_one_iff_of_isLocalRing_isDomain` 📖	mathematical	—	`ringKrullDim` `CommRing.toCommSemiring` `WithBot` `ENat` `WithBot.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `IsField` `Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `IsLocalRing.maximalIdeal` `Ideal.radical` `Ideal.span` `Set` `Set.instSingletonSet`	—	`zero_ne_one` `NeZero.charZero_one` `WithBot.charZero` `ringKrullDim_eq_zero_of_isField` `Ideal.radical_eq_sInf` `le_sInf` `Ring.krullDimLE_one_iff_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `Ring.krullDimLE_iff` `Nat.cast_one` `le_of_eq` `IsLocalRing.eq_maximalIdeal` `Ring.KrullDimLE.isField_of_isDomain` `by_contradiction` `le_antisymm` `bot_le` `le_trans` `Ideal.IsRadical.radical_le_iff` `Ideal.IsPrime.isRadical` `Ideal.span_singleton_le_iff_mem` `Ideal.IsMaximal.eq_of_le` `IsLocalRing.maximalIdeal.isMaximal` `Ideal.IsPrime.ne_top` `Order.succ_le_of_lt` `lt_of_not_ge`

---