Documentation Verification Report

Defs

📁 Source: Mathlib/GroupTheory/Abelianization/Defs.lean

Statistics

Metric	Count
Definitions `Abelianization`, `commGroup`, `equivOfComm`, `instInhabited`, `map`, `of`, `abelianizationCongr`, `instUniqueAbelianization`	8
Theorems `coe_lift_symm`, `commutator_subset_ker`, `equivOfComm_apply`, `equivOfComm_symm_apply`, `hom_ext`, `hom_ext_iff`, `ker_of`, `lift_apply_of`, `lift_of`, `lift_of_comp`, `lift_symm_apply`, `lift_unique`, `map_comp`, `map_id`, `map_map_apply`, `map_of`, `mk_eq_of`, `abelianizationCongr_of`, `abelianizationCongr_refl`, `abelianizationCongr_symm`, `abelianizationCongr_trans`	21
Total	29

Abelianization

Definitions

Name	Category	Theorems
`commGroup` 📖	CompOp	27 math math: `abelianizationCongr_trans`, `hom_ext_iff`, `mk_eq_of`, `map_map_apply`, `FreeAbelianGroup.liftAddEquiv_symm_apply`, `map_of`, `coe_lift_symm`, `lift_apply_of`, `lift_of_comp`, `groupHomology.H1AddEquivOfIsTrivial_single`, `IsZGroup.isCyclic_abelianization`, `map_comp`, `groupHomology.H1AddEquivOfIsTrivial_symm_apply`, `groupHomology.H1ToTensorOfIsTrivial_H1π_single`, `abelianizationCongr_symm`, `abelianizationCongr_refl`, `equivOfComm_apply`, `groupHomology.H1AddEquivOfIsTrivial_apply`, `lift_of`, `abelianizationCongr_of`, `map_id`, `groupHomology.mkH1OfIsTrivial_apply`, `FreeAbelianGroup.liftAddEquiv_apply_apply`, `lift_symm_apply`, `ker_of`, `groupHomology.H1AddEquivOfIsTrivial_symm_tmul`, `equivOfComm_symm_apply`
`equivOfComm` 📖	CompOp	2 math math: `equivOfComm_apply`, `equivOfComm_symm_apply`
`instInhabited` 📖	CompOp	—
`map` 📖	CompOp	5 math math: `map_map_apply`, `map_of`, `lift_of_comp`, `map_comp`, `map_id`
`of` 📖	CompOp	16 math math: `hom_ext_iff`, `mk_eq_of`, `FreeAbelianGroup.liftAddEquiv_symm_apply`, `map_of`, `coe_lift_symm`, `lift_apply_of`, `lift_of_comp`, `groupHomology.H1AddEquivOfIsTrivial_single`, `groupHomology.H1ToTensorOfIsTrivial_H1π_single`, `equivOfComm_apply`, `lift_of`, `abelianizationCongr_of`, `groupHomology.mkH1OfIsTrivial_apply`, `lift_symm_apply`, `ker_of`, `groupHomology.H1AddEquivOfIsTrivial_symm_tmul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_lift_symm` 📖	mathematical	—	`DFunLike.coe` `Equiv` `MonoidHom` `Abelianization` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `commGroup` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `lift` `MonoidHom.comp` `of`	—	—
`commutator_subset_ker` 📖	mathematical	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `commutator` `MonoidHom.ker` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	`commutator_eq_closure` `Subgroup.closure_le` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `map_inv` `mul_right_comm` `mul_inv_cancel` `one_mul`
`equivOfComm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Abelianization` `CommGroup.toGroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `commGroup` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `equivOfComm` `MonoidHom` `MonoidHom.instFunLike` `of`	—	—
`equivOfComm_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Abelianization` `CommGroup.toGroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `commGroup` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `equivOfComm` `MonoidHom` `MonoidHom.instFunLike` `Equiv` `Equiv.instEquivLike` `lift` `MonoidHom.id`	—	—
`hom_ext` 📖	—	`MonoidHom.comp` `Abelianization` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `commGroup` `of`	—	—	`MonoidHom.ext` `QuotientGroup.induction_on` `DFunLike.congr_fun`
`hom_ext_iff` 📖	mathematical	—	`MonoidHom.comp` `Abelianization` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `commGroup` `of`	—	`hom_ext`
`ker_of` 📖	mathematical	—	`MonoidHom.ker` `Abelianization` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `commGroup` `of` `commutator`	—	`QuotientGroup.ker_mk'`
`lift_apply_of` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Abelianization` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `commGroup` `MonoidHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `of`	—	—
`lift_of` 📖	mathematical	—	`DFunLike.coe` `Equiv` `MonoidHom` `Abelianization` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `commGroup` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `of` `MonoidHom.id`	—	`Equiv.apply_symm_apply`
`lift_of_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `MonoidHom` `Abelianization` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `commGroup` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `MonoidHom.comp` `of` `map`	—	—
`lift_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `MonoidHom` `Abelianization` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `commGroup` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `lift` `MonoidHom.comp` `of`	—	—
`lift_unique` 📖	mathematical	`DFunLike.coe` `MonoidHom` `Abelianization` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `commGroup` `MonoidHom.instFunLike` `of`	`Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift`	—	`QuotientGroup.induction_on`
`map_comp` 📖	mathematical	—	`MonoidHom.comp` `Abelianization` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `commGroup` `map`	—	`hom_ext`
`map_id` 📖	mathematical	—	`map` `MonoidHom.id` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Abelianization` `CommGroup.toGroup` `commGroup`	—	`hom_ext`
`map_map_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Abelianization` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `commGroup` `MonoidHom.instFunLike` `map` `MonoidHom.comp`	—	`DFunLike.congr_fun` `map_comp`
`map_of` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Abelianization` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `commGroup` `MonoidHom.instFunLike` `map` `of`	—	—
`mk_eq_of` 📖	mathematical	—	`QuotientGroup.leftRel` `commutator` `DFunLike.coe` `MonoidHom` `Abelianization` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `commGroup` `MonoidHom.instFunLike` `of`	—	—

MulEquiv

Definitions

Name	Category	Theorems
`abelianizationCongr` 📖	CompOp	4 math math: `abelianizationCongr_trans`, `abelianizationCongr_symm`, `abelianizationCongr_refl`, `abelianizationCongr_of`

(root)

Definitions

Name	Category	Theorems
`Abelianization` 📖	CompOp	29 math math: `abelianizationCongr_trans`, `instFiniteAbelianization`, `Abelianization.hom_ext_iff`, `Abelianization.mk_eq_of`, `Abelianization.map_map_apply`, `FreeAbelianGroup.liftAddEquiv_symm_apply`, `Abelianization.map_of`, `Abelianization.coe_lift_symm`, `Abelianization.lift_apply_of`, `Abelianization.lift_of_comp`, `groupHomology.H1AddEquivOfIsTrivial_single`, `Cardinal.mk_abelianization_le`, `IsZGroup.isCyclic_abelianization`, `Abelianization.map_comp`, `groupHomology.H1AddEquivOfIsTrivial_symm_apply`, `groupHomology.H1ToTensorOfIsTrivial_H1π_single`, `abelianizationCongr_symm`, `abelianizationCongr_refl`, `Abelianization.equivOfComm_apply`, `groupHomology.H1AddEquivOfIsTrivial_apply`, `Abelianization.lift_of`, `abelianizationCongr_of`, `Abelianization.map_id`, `groupHomology.mkH1OfIsTrivial_apply`, `FreeAbelianGroup.liftAddEquiv_apply_apply`, `Abelianization.lift_symm_apply`, `Abelianization.ker_of`, `groupHomology.H1AddEquivOfIsTrivial_symm_tmul`, `Abelianization.equivOfComm_symm_apply`
`instUniqueAbelianization` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abelianizationCongr_of` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Abelianization` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Abelianization.commGroup` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.abelianizationCongr` `MonoidHom` `MonoidHom.instFunLike` `Abelianization.of`	—	—
`abelianizationCongr_refl` 📖	mathematical	—	`MulEquiv.abelianizationCongr` `MulEquiv.refl` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Abelianization` `CommGroup.toGroup` `Abelianization.commGroup`	—	`MulEquiv.toMonoidHom_injective` `Abelianization.lift_of`
`abelianizationCongr_symm` 📖	mathematical	—	`MulEquiv.symm` `Abelianization` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Abelianization.commGroup` `MulEquiv.abelianizationCongr`	—	—
`abelianizationCongr_trans` 📖	mathematical	—	`MulEquiv.trans` `Abelianization` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Abelianization.commGroup` `MulEquiv.abelianizationCongr`	—	`MulEquiv.toMonoidHom_injective` `Abelianization.hom_ext`

---

← Back to Index