Defs

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

Statistics

Metric	Count
Definitions	0
Theorems simple, isSimpleRing_iff	2
Total	2

IsSimpleRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
simple 📖	mathematical	—	IsSimpleOrder TwoSidedIdeal Preorder.toLE PartialOrder.toPreorder TwoSidedIdeal.instPartialOrder CompleteLattice.toBoundedOrder TwoSidedIdeal.instCompleteLattice	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSimpleRing_iff 📖	mathematical	—	IsSimpleRing IsSimpleOrder TwoSidedIdeal Preorder.toLE PartialOrder.toPreorder TwoSidedIdeal.instPartialOrder CompleteLattice.toBoundedOrder TwoSidedIdeal.instCompleteLattice	—	—

---

← Back to Index