FinitelyPresentedGroup

📁 Source: Mathlib/GroupTheory/FinitelyPresentedGroup.lean

Statistics

Metric	Count
Definitions IsFinitelyPresented, IsNormalClosureFG	2
Theorems equiv, out, isFinitelyPresented_iff, map	4
Total	6

Group

Definitions

Name	Category	Theorems
IsFinitelyPresented 📖	CompData	2 math math: IsFinitelyPresented.equiv, isFinitelyPresented_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isFinitelyPresented_iff 📖	mathematical	—	IsFinitelyPresented MonoidHom FreeGroup MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid toDivInvMonoid FreeGroup.instGroup DFunLike.coe MonoidHom.instFunLike Subgroup.IsNormalClosureFG MonoidHom.ker	—	—

Group.IsFinitelyPresented

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equiv 📖	mathematical	—	Group.IsFinitelyPresented	—	MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass MulEquiv.surjective MonoidHom.ker_mulEquiv_comp
out 📖	mathematical	—	MonoidHom FreeGroup MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid FreeGroup.instGroup DFunLike.coe MonoidHom.instFunLike Subgroup.IsNormalClosureFG MonoidHom.ker	—	—

Subgroup

Definitions

Name	Category	Theorems
IsNormalClosureFG 📖	MathDef	3 math math: IsNormalClosureFG.map, Group.IsFinitelyPresented.out, Group.isFinitelyPresented_iff

Subgroup.IsNormalClosureFG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map 📖	mathematical	Subgroup.IsNormalClosureFG DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike	Subgroup.IsNormalClosureFG Subgroup.map	—	Set.Finite.image Subgroup.map_normalClosure

---

← Back to Index