PID

📁 Source: Mathlib/RingTheory/KrullDimension/PID.lean

Statistics

Metric	Count
Definitions	0
Theorems height_eq_one_of_isMaximal, krullDimLE_one, ringKrullDim_eq_one	3
Total	3

IsPrincipalIdealRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
height_eq_one_of_isMaximal 📖	mathematical	IsField CommSemiring.toSemiring CommRing.toCommSemiring	Ideal.height ENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instCommSemiringENat	—	le_antisymm ringKrullDim_eq_one Ideal.height_le_ringKrullDim_of_ne_top Ideal.IsPrime.ne_top' Ideal.IsMaximal.isPrime' Nat.cast_one Order.one_le_iff_pos IsOrderedRing.toZeroLEOneClass NeZero.one Ideal.height_eq_primeHeight Ideal.primeHeight.eq_1 Order.height_pos not_isMin_of_lt Ideal.bot_lt_of_maximal IsDomain.toNontrivial
krullDimLE_one 📖	mathematical	—	Ring.KrullDimLE CommRing.toCommSemiring	—	Ring.krullDimLE_one_iff not_minimal_iff_exists_lt Set.notMem_setOf_iff minimalPrimes_eq_minimals of_surjective Ideal.instIsTwoSided_1 RingHom.instRingHomClass Ideal.Quotient.mk_surjective Ideal.map_isPrime_of_surjective Ideal.mk_ker LT.lt.le IsPrime.to_maximal_ideal Ideal.Quotient.isDomain Ideal.map_eq_bot_iff_le_ker LT.lt.not_ge Ideal.comap_isMaximal_of_surjective Ideal.comap_map_of_surjective' sup_of_le_left
ringKrullDim_eq_one 📖	mathematical	IsField CommSemiring.toSemiring CommRing.toCommSemiring	ringKrullDim WithBot ENat WithBot.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instCommSemiringENat	—	eq_of_le_of_not_lt Nat.cast_one Ring.krullDimLE_iff krullDimLE_one Order.le_of_lt_succ Ring.KrullDimLE.isField_of_isDomain Nat.cast_zero

---

← Back to Index