Field

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

Statistics

Metric	Count
Definitions	0
Theorems isField_center, isSimpleRing_iff_isField	2
Total	2

IsSimpleRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isField_center 📖	mathematical	—	IsField Subring SetLike.instMembership Subring.instSetLike Subring.center CommSemiring.toSemiring CommRing.toCommSemiring Subring.instCommRingSubtypeMemCenter	—	AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass SubringClass.toSubsemiringClass Subring.instSubringClass AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass zero_ne_one NeZero.one Subring.instNontrivialSubtypeMem instNontrivial mul_comm MulZeroClass.mul_zero mul_add Distrib.leftDistribClass mul_neg mul_assoc Subring.mem_center_iff one_mem_of_ne_zero_mem mul_one one_mul

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSimpleRing_iff_isField 📖	mathematical	—	IsSimpleRing NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsField CommSemiring.toSemiring CommRing.toCommSemiring	—	MulEquiv.isField SubringClass.toSubsemiringClass Subring.instSubringClass Subring.center_eq_top IsSimpleRing.isField_center DivisionRing.isSimpleRing

---

← Back to Index