PresentedGroup

📁 Source: Mathlib/GroupTheory/PresentedGroup.lean

Statistics

Metric	Count
Definitions PresentedGroup, equivPresentedGroup, instGroup, instInhabited, mk, of, toGroup	7
Theorems closure_range_of, closure_rels_subset_ker, equivPresentedGroup_apply_of, equivPresentedGroup_symm_apply_of, ext, ext_iff, generated_by, induction_on, mk_eq_mk_of_inv_mul_mem, mk_eq_mk_of_mul_inv_mem, mk_eq_one_iff, mk_surjective, one_of_mem, of, unique, to_group_eq_one_of_mem_closure	16
Total	23

PresentedGroup

Definitions

Name	Category	Theorems
equivPresentedGroup 📖	CompOp	2 math math: equivPresentedGroup_symm_apply_of, equivPresentedGroup_apply_of
instGroup 📖	CompOp	12 math math: ext_iff, mk_eq_mk_of_mul_inv_mem, mk_eq_one_iff, mk_eq_mk_of_inv_mul_mem, generated_by, mk_surjective, one_of_mem, toGroup.of, closure_range_of, equivPresentedGroup_symm_apply_of, equivPresentedGroup_apply_of, toGroup.unique
instInhabited 📖	CompOp	—
mk 📖	CompOp	—
of 📖	CompOp	5 math math: ext_iff, toGroup.of, closure_range_of, equivPresentedGroup_symm_apply_of, equivPresentedGroup_apply_of
toGroup 📖	CompOp	2 math math: toGroup.of, toGroup.unique

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_range_of 📖	mathematical	—	Subgroup.closure PresentedGroup instGroup Set.range of Top.top Subgroup Subgroup.instTop	—	Subgroup.normalClosure_normal Set.range_comp MonoidHom.map_closure FreeGroup.closure_range_of MonoidHom.range_eq_map MonoidHom.range_eq_top QuotientGroup.mk'_surjective
closure_rels_subset_ker 📖	mathematical	DFunLike.coe MonoidHom FreeGroup MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid FreeGroup.instGroup MonoidHom.instFunLike Equiv EquivLike.toFunLike Equiv.instEquivLike FreeGroup.lift InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	Subgroup FreeGroup FreeGroup.instGroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder Subgroup.normalClosure MonoidHom.ker Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid DFunLike.coe Equiv MonoidHom MulOneClass.toMulOne EquivLike.toFunLike Equiv.instEquivLike FreeGroup.lift	—	Subgroup.normalClosure_le_normal MonoidHom.normal_ker MonoidHom.mem_ker
equivPresentedGroup_apply_of 📖	mathematical	—	DFunLike.coe MulEquiv PresentedGroup Set.image FreeGroup FreeGroup.instMul EquivLike.toFunLike MulEquiv.instEquivLike FreeGroup.freeGroupCongr MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup equivPresentedGroup of Equiv Equiv.instEquivLike	—	—
equivPresentedGroup_symm_apply_of 📖	mathematical	—	DFunLike.coe MulEquiv PresentedGroup Set.image FreeGroup FreeGroup.instMul EquivLike.toFunLike MulEquiv.instEquivLike FreeGroup.freeGroupCongr MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MulEquiv.symm equivPresentedGroup of Equiv Equiv.instEquivLike Equiv.symm	—	—
ext 📖	—	DFunLike.coe MonoidHom PresentedGroup MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MonoidHom.instFunLike of	—	—	QuotientGroup.monoidHom_ext FreeGroup.ext_hom
ext_iff 📖	mathematical	—	DFunLike.coe MonoidHom PresentedGroup MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MonoidHom.instFunLike of	—	ext
generated_by 📖	mathematical	PresentedGroup Subgroup instGroup SetLike.instMembership Subgroup.instSetLike of	PresentedGroup Subgroup instGroup SetLike.instMembership Subgroup.instSetLike	—	FreeGroup.induction_on OneMemClass.one_mem SubmonoidClass.toOneMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass Subgroup.inv_mem_iff Subgroup.normalClosure_normal QuotientGroup.mk_mul Subgroup.mul_mem
induction_on 📖	—	DFunLike.coe MonoidHom FreeGroup PresentedGroup MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid FreeGroup.instGroup instGroup MonoidHom.instFunLike	—	—	Quotient.inductionOn'
mk_eq_mk_of_inv_mul_mem 📖	mathematical	FreeGroup Set Set.instMembership FreeGroup.instMul FreeGroup.instInv	DFunLike.coe MonoidHom FreeGroup PresentedGroup MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid FreeGroup.instGroup instGroup MonoidHom.instFunLike	—	eq_of_inv_mul_eq_one one_of_mem
mk_eq_mk_of_mul_inv_mem 📖	mathematical	FreeGroup Set Set.instMembership FreeGroup.instMul FreeGroup.instInv	DFunLike.coe MonoidHom FreeGroup PresentedGroup MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid FreeGroup.instGroup instGroup MonoidHom.instFunLike	—	eq_of_mul_inv_eq_one one_of_mem
mk_eq_one_iff 📖	mathematical	—	DFunLike.coe MonoidHom FreeGroup PresentedGroup MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid FreeGroup.instGroup instGroup MonoidHom.instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.normalClosure	—	QuotientGroup.eq_one_iff
mk_surjective 📖	mathematical	—	FreeGroup PresentedGroup DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid FreeGroup.instGroup instGroup MonoidHom.instFunLike	—	QuotientGroup.mk_surjective
one_of_mem 📖	mathematical	FreeGroup Set Set.instMembership	DFunLike.coe MonoidHom FreeGroup PresentedGroup MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid FreeGroup.instGroup instGroup MonoidHom.instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	mk_eq_one_iff Subgroup.subset_normalClosure
to_group_eq_one_of_mem_closure 📖	mathematical	DFunLike.coe MonoidHom FreeGroup MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid FreeGroup.instGroup MonoidHom.instFunLike Equiv EquivLike.toFunLike Equiv.instEquivLike FreeGroup.lift InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.normalClosure	DFunLike.coe MonoidHom FreeGroup MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid FreeGroup.instGroup MonoidHom.instFunLike Equiv EquivLike.toFunLike Equiv.instEquivLike FreeGroup.lift InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	MonoidHom.mem_ker closure_rels_subset_ker

PresentedGroup.toGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of 📖	mathematical	DFunLike.coe MonoidHom FreeGroup MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid FreeGroup.instGroup MonoidHom.instFunLike Equiv EquivLike.toFunLike Equiv.instEquivLike FreeGroup.lift InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	DFunLike.coe MonoidHom PresentedGroup MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid PresentedGroup.instGroup MonoidHom.instFunLike PresentedGroup.toGroup PresentedGroup.of	—	FreeGroup.lift_apply_of
unique 📖	mathematical	DFunLike.coe MonoidHom FreeGroup MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid FreeGroup.instGroup MonoidHom.instFunLike Equiv EquivLike.toFunLike Equiv.instEquivLike FreeGroup.lift InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid PresentedGroup PresentedGroup.instGroup PresentedGroup.of	DFunLike.coe MonoidHom PresentedGroup MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid PresentedGroup.instGroup MonoidHom.instFunLike PresentedGroup.toGroup	—	QuotientGroup.induction_on FreeGroup.lift_unique

(root)

Definitions

Name	Category	Theorems
PresentedGroup 📖	CompOp	12 math math: PresentedGroup.ext_iff, PresentedGroup.mk_eq_mk_of_mul_inv_mem, PresentedGroup.mk_eq_one_iff, PresentedGroup.mk_eq_mk_of_inv_mul_mem, PresentedGroup.generated_by, PresentedGroup.mk_surjective, PresentedGroup.one_of_mem, PresentedGroup.toGroup.of, PresentedGroup.closure_range_of, PresentedGroup.equivPresentedGroup_symm_apply_of, PresentedGroup.equivPresentedGroup_apply_of, PresentedGroup.toGroup.unique

---

← Back to Index