IntermediateField

📁 Source: Mathlib/Algebra/CharP/IntermediateField.lean

Statistics

Metric	Count
Definitions	0
Theorems charP, charP', charZero, expChar, expChar'	5
Total	5

IntermediateField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
charP 📖	mathematical	—	CharP IntermediateField SetLike.instMembership instSetLike AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing toField	—	charP_of_injective_algebraMap IsScalarTower.left RingHom.injective DivisionRing.isSimpleRing SubsemiringClass.nontrivial SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass IsLocalRing.toNontrivial Field.instIsLocalRing
charP' 📖	mathematical	—	CharP IntermediateField SetLike.instMembership instSetLike AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing toField	—	Subfield.charP
charZero 📖	mathematical	—	CharZero IntermediateField SetLike.instMembership instSetLike AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing toField	—	charZero_of_injective_algebraMap IsScalarTower.left RingHom.injective DivisionRing.isSimpleRing SubsemiringClass.nontrivial SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass IsLocalRing.toNontrivial Field.instIsLocalRing
expChar 📖	mathematical	—	ExpChar IntermediateField SetLike.instMembership instSetLike AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing toField	—	expChar_of_injective_algebraMap IsScalarTower.left RingHom.injective DivisionRing.isSimpleRing SubsemiringClass.nontrivial SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass IsLocalRing.toNontrivial Field.instIsLocalRing
expChar' 📖	mathematical	—	ExpChar IntermediateField SetLike.instMembership instSetLike AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing toField	—	Subfield.expChar

---

← Back to Index