Documentation Verification Report

Defs

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

Statistics

Metric	Count
Definitions `AddGroupExtension`, `symm_apply`, `instEquivLike`, `refl`, `toAddEquiv`, `trans`, `IsAddConj`, `instFunLike`, `toFun`, `Splitting`, `instFunLike`, `toAddMonoidHom`, `toSection`, `inl`, `rightHom`, `GroupExtension`, `symm_apply`, `instEquivLike`, `refl`, `toMulEquiv`, `trans`, `IsConj`, `instFunLike`, `toFun`, `Splitting`, `instFunLike`, `toMonoidHom`, `toSection`, `conjAct`, `inl`, `rightHom`, `inr_splitting`, `toGroupExtension`	33
Theorems `coe_symm`, `coe_toAddEquiv`, `inl_comm`, `instAddEquivClass`, `map_inl`, `refl_apply`, `refl_symm_apply`, `rightHom_comm`, `rightHom_map`, `symm_symm_apply`, `toAddEquiv_eq_coe`, `trans_apply`, `trans_symm_apply`, `coe_mk`, `rightHom_comp_section`, `rightHom_section`, `rightInverse_rightHom`, `coe_addMonoidHom_mk`, `coe_mk`, `instAddMonoidHomClass`, `rightHom_comp_splitting`, `rightHom_splitting`, `rightInverse_rightHom`, `inl_injective`, `normal_inl_range`, `range_inl_eq_ker_rightHom`, `rightHom_comp_inl`, `rightHom_inl`, `rightHom_surjective`, `coe_symm`, `coe_toMulEquiv`, `inl_comm`, `instMulEquivClass`, `map_inl`, `refl_apply`, `refl_symm_apply`, `rightHom_comm`, `rightHom_map`, `symm_symm_apply`, `toMulEquiv_eq_coe`, `trans_apply`, `trans_symm_apply`, `coe_mk`, `rightHom_comp_section`, `rightHom_section`, `rightInverse_rightHom`, `coe_mk`, `coe_monoidHom_mk`, `instMonoidHomClass`, `rightHom_comp_splitting`, `rightHom_splitting`, `rightInverse_rightHom`, `inl_conjAct_comm`, `inl_injective`, `normal_inl_range`, `range_inl_eq_ker_rightHom`, `rightHom_comp_inl`, `rightHom_inl`, `rightHom_surjective`, `toGroupExtension_inl`, `toGroupExtension_rightHom`	61
Total	94

AddGroupExtension

Definitions

Name	Category	Theorems
`IsAddConj` 📖	MathDef	3 math math: `IsAddConj.trans`, `IsAddConj.symm`, `IsAddConj.refl`
`Splitting` 📖	CompData	5 math math: `Splitting.coe_addMonoidHom_mk`, `Splitting.rightHom_splitting`, `Splitting.instAddMonoidHomClass`, `Splitting.coe_mk`, `Splitting.rightHom_comp_splitting`
`inl` 📖	CompOp	15 math math: `Section.exists_eq_inl_add`, `Equiv.map_inl`, `range_inl_eq_ker_rightHom`, `rightHom_inl`, `Section.exists_add_eq_inl_add_add`, `normal_inl_range`, `Section.add_add_add_neg_mem_range_inl`, `inl_injective`, `Section.exists_add_eq_add_add_inl`, `Equiv.inl_comm`, `rightHom_comp_inl`, `Section.add_neg_mem_range_inl`, `Section.neg_add_mem_range_inl`, `Section.add_neg_add_add_mem_range_inl`, `Section.exists_eq_add_inl`
`rightHom` 📖	CompOp	12 math math: `range_inl_eq_ker_rightHom`, `rightHom_inl`, `Splitting.rightHom_splitting`, `Equiv.rightHom_comm`, `Section.rightHom_comp_section`, `Section.rightHom_section`, `Section.rightInverse_rightHom`, `Equiv.rightHom_map`, `rightHom_comp_inl`, `rightHom_surjective`, `Splitting.rightHom_comp_splitting`, `Splitting.rightInverse_rightHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inl_injective` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `inl`	—	—
`normal_inl_range` 📖	mathematical	—	`AddSubgroup.Normal` `AddMonoidHom.range` `inl`	—	`AddMonoidHom.normal_ker` `range_inl_eq_ker_rightHom`
`range_inl_eq_ker_rightHom` 📖	mathematical	—	`AddMonoidHom.range` `inl` `AddMonoidHom.ker` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `rightHom`	—	—
`rightHom_comp_inl` 📖	mathematical	—	`AddMonoidHom.comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `rightHom` `inl` `AddMonoidHom` `instZeroAddMonoidHom`	—	`AddMonoidHom.ext` `AddMonoidHom.zero_apply` `AddMonoidHom.comp_apply` `rightHom_inl`
`rightHom_inl` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `rightHom` `inl` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`AddMonoidHom.mem_ker` `range_inl_eq_ker_rightHom` `AddMonoidHom.mem_range`
`rightHom_surjective` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `rightHom`	—	—

AddGroupExtension.Equiv

Definitions

Name	Category	Theorems
`instEquivLike` 📖	CompOp	12 math math: `refl_apply`, `map_inl`, `trans_apply`, `refl_symm_apply`, `symm_symm_apply`, `coe_symm`, `toAddEquiv_eq_coe`, `AddGroupExtension.Section.equivComp_apply`, `trans_symm_apply`, `coe_toAddEquiv`, `rightHom_map`, `instAddEquivClass`
`refl` 📖	CompOp	2 math math: `refl_apply`, `refl_symm_apply`
`toAddEquiv` 📖	CompOp	3 math math: `rightHom_comm`, `toAddEquiv_eq_coe`, `inl_comm`
`trans` 📖	CompOp	2 math math: `trans_apply`, `trans_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_symm` 📖	mathematical	—	`AddEquiv.symm` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddEquivClass.toAddEquiv` `AddGroupExtension.Equiv` `instEquivLike` `instAddEquivClass` `symm`	—	`instAddEquivClass`
`coe_toAddEquiv` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquivClass.toAddEquiv` `AddGroupExtension.Equiv` `instEquivLike` `instAddEquivClass`	—	`instAddEquivClass`
`inl_comm` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toAddEquiv` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `AddGroupExtension.inl`	—	—
`instAddEquivClass` 📖	mathematical	—	`AddEquivClass` `AddGroupExtension.Equiv` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instEquivLike`	—	`AddEquiv.map_add'`
`map_inl` 📖	mathematical	—	`DFunLike.coe` `AddGroupExtension.Equiv` `EquivLike.toFunLike` `instEquivLike` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `AddGroupExtension.inl`	—	`inl_comm`
`refl_apply` 📖	mathematical	—	`DFunLike.coe` `AddGroupExtension.Equiv` `EquivLike.toFunLike` `instEquivLike` `refl`	—	—
`refl_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddGroupExtension.Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `refl`	—	—
`rightHom_comm` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `AddGroupExtension.rightHom` `AddEquiv` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toAddEquiv`	—	—
`rightHom_map` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `AddGroupExtension.rightHom` `AddGroupExtension.Equiv` `EquivLike.toFunLike` `instEquivLike`	—	`rightHom_comm`
`symm_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddGroupExtension.Equiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	—
`toAddEquiv_eq_coe` 📖	mathematical	—	`toAddEquiv` `AddEquivClass.toAddEquiv` `AddGroupExtension.Equiv` `instEquivLike` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instAddEquivClass`	—	—
`trans_apply` 📖	mathematical	—	`DFunLike.coe` `AddGroupExtension.Equiv` `EquivLike.toFunLike` `instEquivLike` `trans`	—	—
`trans_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddGroupExtension.Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `trans`	—	—

AddGroupExtension.Equiv.Simps

Definitions

Name	Category	Theorems
`symm_apply` 📖	CompOp	—

AddGroupExtension.Section

Definitions

Name	Category	Theorems
`instFunLike` 📖	CompOp	12 math math: `exists_eq_inl_add`, `exists_add_eq_inl_add_add`, `add_add_add_neg_mem_range_inl`, `rightHom_comp_section`, `rightHom_section`, `exists_add_eq_add_add_inl`, `equivComp_apply`, `add_neg_mem_range_inl`, `neg_add_mem_range_inl`, `add_neg_add_add_mem_range_inl`, `coe_mk`, `exists_eq_add_inl`
`toFun` 📖	CompOp	1 math math: `rightInverse_rightHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mk` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `AddGroupExtension.rightHom`	`DFunLike.coe` `AddGroupExtension.Section` `instFunLike`	—	—
`rightHom_comp_section` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `AddGroupExtension.rightHom` `AddGroupExtension.Section` `instFunLike`	—	`Function.RightInverse.comp_eq_id` `rightInverse_rightHom`
`rightHom_section` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `AddGroupExtension.rightHom` `AddGroupExtension.Section` `instFunLike`	—	`rightInverse_rightHom`
`rightInverse_rightHom` 📖	mathematical	—	`toFun` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `AddGroupExtension.rightHom`	—	—

AddGroupExtension.Splitting

Definitions

Name	Category	Theorems
`instFunLike` 📖	CompOp	5 math math: `coe_addMonoidHom_mk`, `rightHom_splitting`, `instAddMonoidHomClass`, `coe_mk`, `rightHom_comp_splitting`
`toAddMonoidHom` 📖	CompOp	1 math math: `rightInverse_rightHom`
`toSection` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_addMonoidHom_mk` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `AddGroupExtension.rightHom`	`AddMonoidHomClass.toAddMonoidHom` `AddGroupExtension.Splitting` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instFunLike` `instAddMonoidHomClass`	—	`instAddMonoidHomClass`
`coe_mk` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `AddGroupExtension.rightHom`	`DFunLike.coe` `AddGroupExtension.Splitting` `instFunLike` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike`	—	—
`instAddMonoidHomClass` 📖	mathematical	—	`AddMonoidHomClass` `AddGroupExtension.Splitting` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instFunLike`	—	`AddMonoidHom.map_add'` `ZeroHom.map_zero'`
`rightHom_comp_splitting` 📖	mathematical	—	`AddMonoidHom.comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddGroupExtension.rightHom` `AddMonoidHomClass.toAddMonoidHom` `AddGroupExtension.Splitting` `instFunLike` `instAddMonoidHomClass` `AddMonoidHom.id`	—	`AddMonoidHom.ext` `instAddMonoidHomClass` `rightHom_splitting`
`rightHom_splitting` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `AddGroupExtension.rightHom` `AddGroupExtension.Splitting` `instFunLike`	—	`rightInverse_rightHom`
`rightInverse_rightHom` 📖	mathematical	—	`ZeroHom.toFun` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.toZeroHom` `toAddMonoidHom` `DFunLike.coe` `AddMonoidHom` `AddMonoidHom.instFunLike` `AddGroupExtension.rightHom`	—	—

GroupExtension

Definitions

Name	Category	Theorems
`IsConj` 📖	MathDef	3 math math: `IsConj.trans`, `IsConj.refl`, `IsConj.symm`
`Splitting` 📖	CompData	6 math math: `Splitting.instMonoidHomClass`, `Splitting.rightHom_comp_splitting`, `Splitting.rightHom_splitting`, `Splitting.coe_mk`, `SemidirectProduct.right_splitting`, `Splitting.coe_monoidHom_mk`
`conjAct` 📖	CompOp	1 math math: `inl_conjAct_comm`
`inl` 📖	CompOp	17 math math: `normal_inl_range`, `Section.mul_inv_mem_range_inl`, `Section.mul_inv_mul_mul_mem_range_inl`, `rightHom_inl`, `Equiv.map_inl`, `Section.exists_mul_eq_mul_mul_inl`, `Section.inv_mul_mem_range_inl`, `Section.exists_eq_inl_mul`, `Section.mul_mul_mul_inv_mem_range_inl`, `Section.exists_mul_eq_inl_mul_mul`, `Equiv.inl_comm`, `Section.exists_eq_mul_inl`, `rightHom_comp_inl`, `inl_conjAct_comm`, `SemidirectProduct.toGroupExtension_inl`, `inl_injective`, `range_inl_eq_ker_rightHom`
`rightHom` 📖	CompOp	13 math math: `rightHom_inl`, `Splitting.rightInverse_rightHom`, `Section.rightHom_section`, `rightHom_surjective`, `Equiv.rightHom_comm`, `rightHom_comp_inl`, `Splitting.rightHom_comp_splitting`, `Equiv.rightHom_map`, `Section.rightInverse_rightHom`, `Splitting.rightHom_splitting`, `Section.rightHom_comp_section`, `SemidirectProduct.toGroupExtension_rightHom`, `range_inl_eq_ker_rightHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inl_conjAct_comm` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `inl` `MulEquiv` `MulOne.toMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulAut` `MulAut.instGroup` `conjAct` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`MonoidHom.apply_ofInjective_symm` `inl_injective` `normal_inl_range`
`inl_injective` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `inl`	—	—
`normal_inl_range` 📖	mathematical	—	`Subgroup.Normal` `MonoidHom.range` `inl`	—	`MonoidHom.normal_ker` `range_inl_eq_ker_rightHom`
`range_inl_eq_ker_rightHom` 📖	mathematical	—	`MonoidHom.range` `inl` `MonoidHom.ker` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `rightHom`	—	—
`rightHom_comp_inl` 📖	mathematical	—	`MonoidHom.comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `rightHom` `inl` `MonoidHom` `instOneMonoidHom`	—	`MonoidHom.ext` `MonoidHom.one_apply` `MonoidHom.comp_apply` `rightHom_inl`
`rightHom_inl` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `rightHom` `inl` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`MonoidHom.mem_ker` `range_inl_eq_ker_rightHom` `MonoidHom.mem_range`
`rightHom_surjective` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `rightHom`	—	—

GroupExtension.Equiv

Definitions

Name	Category	Theorems
`instEquivLike` 📖	CompOp	12 math math: `toMulEquiv_eq_coe`, `symm_symm_apply`, `map_inl`, `refl_apply`, `coe_symm`, `instMulEquivClass`, `refl_symm_apply`, `coe_toMulEquiv`, `rightHom_map`, `GroupExtension.Section.equivComp_apply`, `trans_apply`, `trans_symm_apply`
`refl` 📖	CompOp	2 math math: `refl_apply`, `refl_symm_apply`
`toMulEquiv` 📖	CompOp	3 math math: `toMulEquiv_eq_coe`, `rightHom_comm`, `inl_comm`
`trans` 📖	CompOp	2 math math: `trans_apply`, `trans_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_symm` 📖	mathematical	—	`MulEquiv.symm` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulEquivClass.toMulEquiv` `GroupExtension.Equiv` `instEquivLike` `instMulEquivClass` `symm`	—	`instMulEquivClass`
`coe_toMulEquiv` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquivClass.toMulEquiv` `GroupExtension.Equiv` `instEquivLike` `instMulEquivClass`	—	`instMulEquivClass`
`inl_comm` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `toMulEquiv` `MonoidHom` `MonoidHom.instFunLike` `GroupExtension.inl`	—	—
`instMulEquivClass` 📖	mathematical	—	`MulEquivClass` `GroupExtension.Equiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instEquivLike`	—	`MulEquiv.map_mul'`
`map_inl` 📖	mathematical	—	`DFunLike.coe` `GroupExtension.Equiv` `EquivLike.toFunLike` `instEquivLike` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `GroupExtension.inl`	—	`inl_comm`
`refl_apply` 📖	mathematical	—	`DFunLike.coe` `GroupExtension.Equiv` `EquivLike.toFunLike` `instEquivLike` `refl`	—	—
`refl_symm_apply` 📖	mathematical	—	`DFunLike.coe` `GroupExtension.Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `refl`	—	—
`rightHom_comm` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `GroupExtension.rightHom` `MulEquiv` `MulOne.toMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `toMulEquiv`	—	—
`rightHom_map` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `GroupExtension.rightHom` `GroupExtension.Equiv` `EquivLike.toFunLike` `instEquivLike`	—	`rightHom_comm`
`symm_symm_apply` 📖	mathematical	—	`DFunLike.coe` `GroupExtension.Equiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	—
`toMulEquiv_eq_coe` 📖	mathematical	—	`toMulEquiv` `MulEquivClass.toMulEquiv` `GroupExtension.Equiv` `instEquivLike` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instMulEquivClass`	—	—
`trans_apply` 📖	mathematical	—	`DFunLike.coe` `GroupExtension.Equiv` `EquivLike.toFunLike` `instEquivLike` `trans`	—	—
`trans_symm_apply` 📖	mathematical	—	`DFunLike.coe` `GroupExtension.Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `trans`	—	—

GroupExtension.Equiv.Simps

Definitions

Name	Category	Theorems
`symm_apply` 📖	CompOp	—

GroupExtension.Section

Definitions

Name	Category	Theorems
`instFunLike` 📖	CompOp	12 math math: `mul_inv_mem_range_inl`, `mul_inv_mul_mul_mem_range_inl`, `coe_mk`, `exists_mul_eq_mul_mul_inl`, `inv_mul_mem_range_inl`, `exists_eq_inl_mul`, `rightHom_section`, `mul_mul_mul_inv_mem_range_inl`, `exists_mul_eq_inl_mul_mul`, `exists_eq_mul_inl`, `rightHom_comp_section`, `equivComp_apply`
`toFun` 📖	CompOp	1 math math: `rightInverse_rightHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mk` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `GroupExtension.rightHom`	`DFunLike.coe` `GroupExtension.Section` `instFunLike`	—	—
`rightHom_comp_section` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `GroupExtension.rightHom` `GroupExtension.Section` `instFunLike`	—	`Function.RightInverse.comp_eq_id` `rightInverse_rightHom`
`rightHom_section` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `GroupExtension.rightHom` `GroupExtension.Section` `instFunLike`	—	`rightInverse_rightHom`
`rightInverse_rightHom` 📖	mathematical	—	`toFun` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `GroupExtension.rightHom`	—	—

GroupExtension.Splitting

Definitions

Name	Category	Theorems
`instFunLike` 📖	CompOp	6 math math: `instMonoidHomClass`, `rightHom_comp_splitting`, `rightHom_splitting`, `coe_mk`, `SemidirectProduct.right_splitting`, `coe_monoidHom_mk`
`toMonoidHom` 📖	CompOp	1 math math: `rightInverse_rightHom`
`toSection` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mk` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `GroupExtension.rightHom`	`DFunLike.coe` `GroupExtension.Splitting` `instFunLike` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	—	—
`coe_monoidHom_mk` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `GroupExtension.rightHom`	`MonoidHomClass.toMonoidHom` `GroupExtension.Splitting` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instFunLike` `instMonoidHomClass`	—	`instMonoidHomClass`
`instMonoidHomClass` 📖	mathematical	—	`MonoidHomClass` `GroupExtension.Splitting` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instFunLike`	—	`MonoidHom.map_mul'` `OneHom.map_one'`
`rightHom_comp_splitting` 📖	mathematical	—	`MonoidHom.comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `GroupExtension.rightHom` `MonoidHomClass.toMonoidHom` `GroupExtension.Splitting` `instFunLike` `instMonoidHomClass` `MonoidHom.id`	—	`MonoidHom.ext` `instMonoidHomClass` `rightHom_splitting`
`rightHom_splitting` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `GroupExtension.rightHom` `GroupExtension.Splitting` `instFunLike`	—	`rightInverse_rightHom`
`rightInverse_rightHom` 📖	mathematical	—	`OneHom.toFun` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.toOneHom` `toMonoidHom` `DFunLike.coe` `MonoidHom` `MonoidHom.instFunLike` `GroupExtension.rightHom`	—	—

SemidirectProduct

Definitions

Name	Category	Theorems
`inr_splitting` 📖	CompOp	—
`toGroupExtension` 📖	CompOp	3 math math: `toGroupExtension_inl`, `toGroupExtension_rightHom`, `right_splitting`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toGroupExtension_inl` 📖	mathematical	—	`GroupExtension.inl` `SemidirectProduct` `instGroup` `toGroupExtension` `inl`	—	—
`toGroupExtension_rightHom` 📖	mathematical	—	`GroupExtension.rightHom` `SemidirectProduct` `instGroup` `toGroupExtension` `rightHom`	—	—

(root)

Definitions

Name	Category	Theorems
`AddGroupExtension` 📖	CompData	—
`GroupExtension` 📖	CompData	—

---

← Back to Index