Principal

📁 Source: Mathlib/RingTheory/SimpleRing/Principal.lean

Statistics

Metric	Count
Definitions	0
Theorems of_isSimpleRing, of_isSimpleRing, instIsSimpleOrderIdeal	3
Total	3

IsDomain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isSimpleRing 📖	mathematical	—	IsDomain CommSemiring.toSemiring CommRing.toCommSemiring	—	IsField.isDomain isSimpleRing_iff_isField

IsPrincipalIdealRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isSimpleRing 📖	mathematical	—	IsPrincipalIdealRing CommSemiring.toSemiring CommRing.toCommSemiring	—	IsField.isPrincipalIdealRing isSimpleRing_iff_isField

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsSimpleOrderIdeal 📖	mathematical	—	IsSimpleOrder Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule CompleteLattice.toBoundedOrder Submodule.completeLattice	—	OrderIso.isSimpleOrder IsSimpleRing.simple

---

← Back to Index