Documentation Verification Report

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	10 math math: `ext_iff`, `mk_eq_mk_of_mul_inv_mem`, `mk_eq_one_iff`, `mk_eq_mk_of_inv_mul_mem`, `mk_surjective`, `one_of_mem`, `toGroup.of`, `closure_range_of`, `equivPresentedGroup_symm_apply_of`, `equivPresentedGroup_apply_of`
`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` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.normalClosure` `MonoidHom.ker`	—	`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` 📖	—	`PresentedGroup` `Subgroup` `instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `of`	—	—	`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` `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` `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` `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` 📖	—	`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`	—	—	`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`	`PresentedGroup` `PresentedGroup.instGroup` `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`	`PresentedGroup.toGroup`	—	`QuotientGroup.induction_on` `FreeGroup.lift_unique`

(root)

Definitions

Name	Category	Theorems
`PresentedGroup` 📖	CompOp	10 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.mk_surjective`, `PresentedGroup.one_of_mem`, `PresentedGroup.toGroup.of`, `PresentedGroup.closure_range_of`, `PresentedGroup.equivPresentedGroup_symm_apply_of`, `PresentedGroup.equivPresentedGroup_apply_of`

---

← Back to Index