Subring

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

Statistics

Metric	Count
Definitions	0
Theorems charP_center_iff, subring, subring', subsemiring, expChar_center_iff	5
Total	5

CharP

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
charP_center_iff 📖	mathematical	—	CharP Subring SetLike.instMembership Subring.instSetLike Subring.center AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Subring.toRing	—	RingHom.charP_iff Subtype.val_injective
subring 📖	mathematical	—	CharP Subring SetLike.instMembership Subring.instSetLike AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Subring.toRing	—	cast_eq_zero_iff map_natCast RingHom.instRingHomClass map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass
subring' 📖	mathematical	—	CharP Subring CommRing.toRing SetLike.instMembership Subring.instSetLike AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Subring.toRing	—	subring
subsemiring 📖	mathematical	—	CharP Subsemiring Semiring.toNonAssocSemiring SetLike.instMembership Subsemiring.instSetLike AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Subsemiring.toNonAssocSemiring	—	cast_eq_zero_iff map_natCast RingHom.instRingHomClass map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass

ExpChar

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
expChar_center_iff 📖	mathematical	—	ExpChar Subring SetLike.instMembership Subring.instSetLike Subring.center AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Subring.toRing	—	RingHom.expChar_iff Subtype.val_injective

---

← Back to Index