Documentation Verification Report

IsFreeGroup

📁 Source: Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean

Statistics

Metric	Count
Definitions `FreeGroupBasis`, `instFunLike`, `map`, `ofFreeGroup`, `ofLift`, `ofUniqueLift`, `reindex`, `repr`, `IsFreeGroup`, `basis`, `mulEquiv`, `of`, `toFreeGroup`	13
Theorems `ext_hom`, `injective`, `instIsFreeGroupFreeGroup`, `isFreeGroup`, `lift_apply_apply`, `lift_symm_apply`, `map_apply`, `ofFreeGroup_apply`, `reindex_apply`, `repr_apply_coe`, `ext_hom`, `lift_of`, `lift_symm_apply`, `mulEquiv_def`, `nonempty_basis`, `ofLift`, `ofMulEquiv`, `ofUniqueLift`, `toFreeGroup_apply`, `toFreeGroup_symm_apply`, `unique_lift`	21
Total	34

FreeGroupBasis

Definitions

Name	Category	Theorems
`instFunLike` 📖	CompOp	5 math math: `repr_apply_coe`, `injective`, `reindex_apply`, `ofFreeGroup_apply`, `map_apply`
`map` 📖	CompOp	1 math math: `map_apply`
`ofFreeGroup` 📖	CompOp	1 math math: `ofFreeGroup_apply`
`ofLift` 📖	CompOp	—
`ofUniqueLift` 📖	CompOp	—
`reindex` 📖	CompOp	1 math math: `reindex_apply`
`repr` 📖	CompOp	4 math math: `repr_apply_coe`, `lift_apply_apply`, `IsFreeGroup.mulEquiv_def`, `lift_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext_hom` 📖	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `FreeGroupBasis` `instFunLike`	—	—	`Equiv.injective`
`injective` 📖	mathematical	—	`DFunLike.coe` `FreeGroupBasis` `instFunLike`	—	`MulEquiv.injective` `FreeGroup.of_injective`
`instIsFreeGroupFreeGroup` 📖	mathematical	—	`IsFreeGroup` `FreeGroup` `FreeGroup.instGroup`	—	`isFreeGroup`
`isFreeGroup` 📖	mathematical	—	`IsFreeGroup`	—	`injective`
`lift_apply_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `FreeGroup` `FreeGroup.instGroup` `FreeGroup.lift` `MulEquiv` `MulOne.toMul` `MulEquiv.instEquivLike` `repr`	—	—
`lift_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `lift` `MonoidHom.instFunLike` `MulEquiv` `FreeGroup` `MulOne.toMul` `FreeGroup.instGroup` `MulEquiv.instEquivLike` `MulEquiv.symm` `FreeGroup.instMul` `repr` `FreeGroup.of`	—	—
`map_apply` 📖	mathematical	—	`DFunLike.coe` `FreeGroupBasis` `instFunLike` `map` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike`	—	—
`ofFreeGroup_apply` 📖	mathematical	—	`DFunLike.coe` `FreeGroupBasis` `FreeGroup` `FreeGroup.instGroup` `instFunLike` `ofFreeGroup` `FreeGroup.of`	—	—
`reindex_apply` 📖	mathematical	—	`DFunLike.coe` `FreeGroupBasis` `instFunLike` `reindex` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	—
`repr_apply_coe` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `FreeGroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `FreeGroup.instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `repr` `FreeGroupBasis` `instFunLike` `FreeGroup.of`	—	`MulEquiv.apply_symm_apply`

IsFreeGroup

Definitions

Name	Category	Theorems
`basis` 📖	CompOp	—
`mulEquiv` 📖	CompOp	3 math math: `mulEquiv_def`, `toFreeGroup_symm_apply`, `toFreeGroup_apply`
`of` 📖	CompOp	2 math math: `lift_of`, `lift_symm_apply`
`toFreeGroup` 📖	CompOp	2 math math: `toFreeGroup_symm_apply`, `toFreeGroup_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext_hom` 📖	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `of`	—	—	`Equiv.injective`
`lift_of` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `of`	—	`Equiv.symm_apply_apply`
`lift_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `lift` `MonoidHom.instFunLike` `of`	—	—
`mulEquiv_def` 📖	mathematical	—	`mulEquiv` `MulEquiv.symm` `FreeGroup` `FreeGroupBasis` `nonempty_basis` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `FreeGroup.instMul` `FreeGroupBasis.repr` `Nonempty.some`	—	`nonempty_basis`
`nonempty_basis` 📖	mathematical	—	`FreeGroupBasis`	—	—
`ofLift` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	`IsFreeGroup`	—	`FreeGroupBasis.isFreeGroup`
`ofMulEquiv` 📖	mathematical	—	`IsFreeGroup`	—	`FreeGroupBasis.isFreeGroup`
`ofUniqueLift` 📖	mathematical	`ExistsUnique` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`IsFreeGroup`	—	`FreeGroupBasis.isFreeGroup`
`toFreeGroup_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `FreeGroup` `Generators` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `FreeGroup.instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `toFreeGroup` `MulEquiv.symm` `mulEquiv`	—	—
`toFreeGroup_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `FreeGroup` `Generators` `FreeGroup.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `toFreeGroup` `mulEquiv`	—	—
`unique_lift` 📖	mathematical	—	`ExistsUnique` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`Function.Bijective.existsUnique` `Equiv.bijective`

(root)

Definitions

Name	Category	Theorems
`FreeGroupBasis` 📖	CompData	7 math math: `FreeGroupBasis.repr_apply_coe`, `FreeGroupBasis.injective`, `IsFreeGroup.mulEquiv_def`, `IsFreeGroup.nonempty_basis`, `FreeGroupBasis.reindex_apply`, `FreeGroupBasis.ofFreeGroup_apply`, `FreeGroupBasis.map_apply`
`IsFreeGroup` 📖	CompData	8 math math: `FreeGroupBasis.isFreeGroup`, `FreeGroupBasis.instIsFreeGroupFreeGroup`, `IsFreeGroupoid.SpanningTree.endIsFree`, `subgroupIsFreeOfIsFree`, `IsFreeGroup.ofMulEquiv`, `IsFreeGroup.ofLift`, `IsFreeGroup.ofUniqueLift`, `IsFreeGroupoid.endIsFreeOfConnectedFree`

---

← Back to Index