IsPerfect

📁 Source: Mathlib/GroupTheory/IsPerfect.lean

Statistics

Metric	Count
Definitions IsPerfect	1
Theorems commutator_eq_top, instOfSubsingleton, instQuotientSubgroup, instSubtypeMemSubgroupTop, map, mem_commutator, not_isMulCommutative, not_isNilpotent, not_isSolvable, ofSurjective, range, subsingleton_of_isMulCommutative, top_iff, isPerfect_def, commutator_eq_self, isPerfect_iff	16
Total	17

Group

Definitions

Name	Category	Theorems
IsPerfect 📖	CompData	9 math math: IsPerfect.top_iff, IsPerfect.instSubtypeMemSubgroupTop, IsPerfect.instOfSubsingleton, isPerfect_def, IsPerfect.ofSurjective, IsPerfect.map, IsPerfect.range, Subgroup.isPerfect_iff, IsPerfect.instQuotientSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPerfect_def 📖	mathematical	—	IsPerfect commutator Top.top Subgroup Subgroup.instTop	—	IsPerfect.commutator_eq_top

Group.IsPerfect

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commutator_eq_top 📖	mathematical	—	commutator Top.top Subgroup Subgroup.instTop	—	—
instOfSubsingleton 📖	mathematical	—	Group.IsPerfect	—	Unique.instSubsingleton
instQuotientSubgroup 📖	mathematical	—	Group.IsPerfect HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup QuotientGroup.Quotient.group	—	ofSurjective QuotientGroup.mk'_surjective
instSubtypeMemSubgroupTop 📖	mathematical	—	Group.IsPerfect Subgroup SetLike.instMembership Subgroup.instSetLike Top.top Subgroup.instTop Subgroup.toGroup	—	top_iff
map 📖	mathematical	—	Group.IsPerfect Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.map Subgroup.toGroup	—	Subgroup.isPerfect_iff Subgroup.map_commutator Subgroup.commutator_eq_self
mem_commutator 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike commutator	—	commutator_eq_top
not_isMulCommutative 📖	mathematical	—	IsMulCommutative MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	not_isSolvable CommGroup.isSolvable
not_isNilpotent 📖	mathematical	—	Group.IsNilpotent	—	not_isSolvable IsNilpotent.to_isSolvable
not_isSolvable 📖	mathematical	—	IsSolvable	—	LT.lt.ne IsSolvable.commutator_lt_top_of_nontrivial commutator_eq_top
ofSurjective 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike	Group.IsPerfect	—	top_iff MonoidHom.range_eq_top_of_surjective range
range 📖	mathematical	—	Group.IsPerfect Subgroup SetLike.instMembership Subgroup.instSetLike MonoidHom.range Subgroup.toGroup	—	MonoidHom.range_eq_map map instSubtypeMemSubgroupTop
subsingleton_of_isMulCommutative 📖	—	—	—	—	not_isMulCommutative
top_iff 📖	mathematical	—	Group.IsPerfect Subgroup SetLike.instMembership Subgroup.instSetLike Top.top Subgroup.instTop Subgroup.toGroup	—	Group.isPerfect_def Subgroup.map_subtype_commutator MonoidHom.range_eq_map Subgroup.subtype_range commutator_def

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commutator_eq_self 📖	mathematical	—	Bracket.bracket Subgroup commutator	—	isPerfect_iff
isPerfect_iff 📖	mathematical	—	Group.IsPerfect Subgroup SetLike.instMembership instSetLike toGroup Bracket.bracket commutator	—	Group.isPerfect_def map_subtype_commutator MonoidHom.range_eq_map range_subtype

---

← Back to Index