Documentation Verification Report

Basic

📁 Source: Mathlib/Algebra/Group/Hom/Basic.lean

Statistics

Metric	Count
Definitions `instAdd`, `add`, `instNeg`, `instSub`, `ofMapAddNeg`, `ofMapSub`, `commGroupOfInjective`, `commGroupOfSurjective`, `instDiv`, `instInv`, `mul`, `ofMapDiv`, `ofMapMulInv`, `instMul`, `instDiv`, `instInv`, `instMul`, `instAdd`, `instNeg`, `instSub`, `invMonoidHom`, `negAddMonoidHom`, `nsmulAddMonoidHom`, `powMonoidHom`, `zpowGroupHom`, `zsmulAddGroupHom`	26
Theorems `add_apply`, `add_comp`, `comp_add`, `add_apply`, `add_comp`, `coe_of_map_add_neg`, `coe_of_map_sub`, `comp_add`, `comp_neg`, `comp_sub`, `neg_apply`, `neg_comp`, `sub_apply`, `sub_comp`, `coe_of_map_div`, `coe_of_map_mul_inv`, `comp_div`, `comp_inv`, `comp_mul`, `div_apply`, `div_comp`, `inv_apply`, `inv_comp`, `mul_apply`, `mul_comp`, `comp_mul`, `mul_apply`, `mul_comp`, `coe_div`, `coe_inv`, `coe_mul`, `div_apply`, `div_comp`, `inv_apply`, `inv_comp`, `mul_apply`, `mul_comp`, `add_apply`, `add_comp`, `coe_add`, `coe_neg`, `coe_sub`, `neg_apply`, `neg_comp`, `sub_apply`, `sub_comp`, `coe_invMonoidHom`, `coe_negAddMonoidHom`, `injective_iff_map_eq_one`, `injective_iff_map_eq_one'`, `injective_iff_map_eq_zero`, `injective_iff_map_eq_zero'`, `invMonoidHom_apply`, `invMonoidHom_comp_invMonoidHom`, `negAddMonoidHom_apply`, `negAddMonoidHom_comp_negAddMonoidHom`, `nsmulAddMonoidHom_apply`, `powMonoidHom_apply`, `zpowGroupHom_apply`, `zsmulAddGroupHom_apply`	60
Total	86

AddHom

Definitions

Name	Category	Theorems
`instAdd` 📖	CompOp	4 math math: `coeFn_apply`, `comp_add`, `add_apply`, `add_comp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`DFunLike.coe` `AddHom` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `funLike` `instAdd`	—	—
`add_comp` 📖	mathematical	—	`comp` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddHom` `instAdd`	—	—
`comp_add` 📖	mathematical	—	`comp` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddHom` `instAdd`	—	`ext` `map_add` `addHomClass`

AddMonoidHom

Definitions

Name	Category	Theorems
`add` 📖	CompOp	46 math math: `DFinsupp.liftAddHom_apply`, `toMultiplicative_add`, `AddCommGrpCat.hom_add`, `DFinsupp.liftAddHom_apply_single`, `instIsCancelAddAddMonoidHom`, `multiplesAddHom_apply`, `FreeAbelianGroup.lift_add`, `zmultiplesAddHom_symm_apply`, `Finsupp.liftAddHom_comp_single`, `multiplesAddHom_symm_apply`, `AddEquiv.symm_addMonoidHomCongrRight`, `FreeAbelianGroup.liftAddEquiv_symm_apply`, `AddEquiv.addMonoidHomCongrLeft_apply`, `Finsupp.comp_liftAddHom`, `AddCommGrpCat.homAddEquiv_symm_apply_hom`, `Finsupp.liftAddHom_apply`, `completion_add`, `instIsRightCancelAddAddMonoidHom`, `AddGroupSeminorm.comp_add_le`, `AddEquiv.addMonoidHomCongrLeft_trans`, `AddEquiv.addMonoidHomCongrRight_trans`, `AddEquiv.addMonoidHomCongrLeft_refl`, `DFinsupp.comp_liftAddHom`, `Finsupp.liftAddHom_singleAddHom`, `DFinsupp.liftAddHom_singleAddHom`, `Finsupp.liftAddHom_apply_single`, `Finsupp.liftAddHom_symm_apply_apply`, `add_apply`, `instIsLeftCancelAddAddMonoidHom`, `mapMatrix_add`, `Finsupp.liftAddHom_symm_apply`, `DFinsupp.liftAddHom_comp_single`, `DFinsupp.sumAddHom_add`, `zmultiplesAddHom_apply`, `FreeAbelianGroup.liftAddEquiv_apply_apply`, `AddEquiv.addMonoidHomCongrRight_refl`, `CategoryTheory.CommShift₂Setup.z_zero₂`, `DFinsupp.liftAddHom_symm_apply`, `AddEquiv.addMonoidHomCongrRight_apply`, `CategoryTheory.CommShift₂Setup.z_zero₁`, `comp_add`, `CategoryTheory.CommShift₂Setup.hε`, `AddCommGrpCat.homAddEquiv_apply`, `add_comp`, `AddEquiv.symm_addMonoidHomCongrLeft`, `CategoryTheory.CommShift₂Setup.int_z`
`instNeg` 📖	CompOp	6 math math: `neg_apply`, `mapMatrix_neg`, `neg_comp`, `comp_neg`, `FreeAbelianGroup.lift_neg`, `AddCommGrpCat.hom_neg`
`instSub` 📖	CompOp	5 math math: `sub_apply`, `AddCommGrpCat.hom_sub`, `mapMatrix_sub`, `comp_sub`, `sub_comp`
`ofMapAddNeg` 📖	CompOp	1 math math: `coe_of_map_add_neg`
`ofMapSub` 📖	CompOp	1 math math: `coe_of_map_sub`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `add` `AddZero.toAdd`	—	—
`add_comp` 📖	mathematical	—	`comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom` `add`	—	—
`coe_of_map_add_neg` 📖	mathematical	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`DFunLike.coe` `AddMonoidHom` `instFunLike` `ofMapAddNeg`	—	—
`coe_of_map_sub` 📖	mathematical	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `instFunLike` `ofMapSub`	—	—
`comp_add` 📖	mathematical	—	`comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom` `add`	—	`ext` `map_add` `AddMonoidHomClass.toAddHomClass` `instAddMonoidHomClass`
`comp_neg` 📖	mathematical	—	`comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoidHom` `instNeg`	—	`ext` `map_neg` `instAddMonoidHomClass`
`comp_sub` 📖	mathematical	—	`comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoidHom` `instSub`	—	`ext` `map_sub` `instAddMonoidHomClass`
`neg_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instFunLike` `instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`neg_comp` 📖	mathematical	—	`comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoidHom` `instNeg`	—	—
`sub_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instFunLike` `instSub` `SubNegMonoid.toSub`	—	—
`sub_comp` 📖	mathematical	—	`comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoidHom` `instSub`	—	—

MonoidHom

Definitions

Name	Category	Theorems
`commGroupOfInjective` 📖	CompOp	—
`commGroupOfSurjective` 📖	CompOp	—
`instDiv` 📖	CompOp	3 math math: `comp_div`, `div_comp`, `div_apply`
`instInv` 📖	CompOp	3 math math: `comp_inv`, `inv_apply`, `inv_comp`
`mul` 📖	CompOp	30 math math: `GroupSeminorm.comp_mul_le`, `zpowersMulHom_symm_apply`, `instIsRightCancelMulMonoidHom`, `MulEquiv.monoidHomCongrLeft_apply`, `AddMonoidHom.toMultiplicative_add`, `restrictHomKerEquiv_apply_coe`, `CommGroup.monoidHom_mulEquiv_of_hasEnoughRootsOfUnity`, `IsCyclic.monoidHom_mulEquiv_rootsOfUnity`, `comp_mul`, `MulEquiv.monoidHomCongrRight_refl`, `zpowersMulHom_apply`, `MulEquiv.symm_monoidHomCongrRight`, `restrictHomKerEquiv_symm_coe_apply`, `MulEquiv.monoidHomCongrLeft_trans`, `IsCyclic.monoidHom_equiv_self`, `toHomUnits_mul`, `MulEquiv.monoidHomCongrLeft_refl`, `powersMulHom_apply`, `AddChar.toMonoidHomEquiv_add`, `MulEquiv.monoidHomCongrRight_trans`, `mul_comp`, `MulEquiv.monoidHomCongrRight_apply`, `AddChar.toMonoidHomEquiv_symm_mul`, `instIsCancelMulMonoidHom`, `MulEquiv.symm_monoidHomCongrLeft`, `instIsLeftCancelMulMonoidHom`, `toHomUnitsMulEquiv_symm_apply`, `powersMulHom_symm_apply`, `mul_apply`, `toHomUnitsMulEquiv_apply`
`ofMapDiv` 📖	CompOp	1 math math: `coe_of_map_div`
`ofMapMulInv` 📖	CompOp	1 math math: `coe_of_map_mul_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_of_map_div` 📖	mathematical	`DivInvMonoid.toDiv` `Group.toDivInvMonoid`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `instFunLike` `ofMapDiv`	—	—
`coe_of_map_mul_inv` 📖	mathematical	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`DFunLike.coe` `MonoidHom` `instFunLike` `ofMapMulInv`	—	—
`comp_div` 📖	mathematical	—	`comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `MonoidHom` `instDiv`	—	`ext` `map_div` `instMonoidHomClass`
`comp_inv` 📖	mathematical	—	`comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `MonoidHom` `instInv`	—	`ext` `map_inv` `instMonoidHomClass`
`comp_mul` 📖	mathematical	—	`comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom` `mul`	—	`ext` `map_mul` `MonoidHomClass.toMulHomClass` `instMonoidHomClass`
`div_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instFunLike` `instDiv` `DivInvMonoid.toDiv`	—	—
`div_comp` 📖	mathematical	—	`comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `MonoidHom` `instDiv`	—	—
`inv_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instFunLike` `instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	—	—
`inv_comp` 📖	mathematical	—	`comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `MonoidHom` `instInv`	—	—
`mul_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instFunLike` `mul` `MulOne.toMul`	—	—
`mul_comp` 📖	mathematical	—	`comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom` `mul`	—	—

MulHom

Definitions

Name	Category	Theorems
`instMul` 📖	CompOp	4 math math: `mul_apply`, `comp_mul`, `coeFn_apply`, `mul_comp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_mul` 📖	mathematical	—	`comp` `CommMagma.toMul` `CommSemigroup.toCommMagma` `MulHom` `instMul`	—	`ext` `map_mul` `mulHomClass`
`mul_apply` 📖	mathematical	—	`DFunLike.coe` `MulHom` `CommMagma.toMul` `CommSemigroup.toCommMagma` `funLike` `instMul`	—	—
`mul_comp` 📖	mathematical	—	`comp` `CommMagma.toMul` `CommSemigroup.toCommMagma` `MulHom` `instMul`	—	—

OneHom

Definitions

Name	Category	Theorems
`instDiv` 📖	CompOp	3 math math: `div_comp`, `coe_div`, `div_apply`
`instInv` 📖	CompOp	3 math math: `inv_apply`, `inv_comp`, `coe_inv`
`instMul` 📖	CompOp	6 math math: `instIsCancelMulOneHom`, `mul_comp`, `coe_mul`, `mul_apply`, `instIsRightCancelMulOneHom`, `instIsLeftCancelMulOneHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_div` 📖	mathematical	—	`DFunLike.coe` `OneHom` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `funLike` `instDiv` `Pi.instDiv` `DivInvMonoid.toDiv` `DivisionMonoid.toDivInvMonoid`	—	—
`coe_inv` 📖	mathematical	—	`DFunLike.coe` `OneHom` `InvOneClass.toOne` `funLike` `instInv` `Pi.instInv` `InvOneClass.toInv`	—	—
`coe_mul` 📖	mathematical	—	`DFunLike.coe` `OneHom` `MulOne.toOne` `MulOneClass.toMulOne` `funLike` `instMul` `Pi.instMul` `MulOne.toMul`	—	—
`div_apply` 📖	mathematical	—	`DFunLike.coe` `OneHom` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `funLike` `instDiv` `DivInvMonoid.toDiv` `DivisionMonoid.toDivInvMonoid`	—	—
`div_comp` 📖	mathematical	—	`comp` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `OneHom` `instDiv`	—	—
`inv_apply` 📖	mathematical	—	`DFunLike.coe` `OneHom` `InvOneClass.toOne` `funLike` `instInv` `InvOneClass.toInv`	—	—
`inv_comp` 📖	mathematical	—	`comp` `InvOneClass.toOne` `OneHom` `instInv`	—	—
`mul_apply` 📖	mathematical	—	`DFunLike.coe` `OneHom` `MulOne.toOne` `MulOneClass.toMulOne` `funLike` `instMul` `MulOne.toMul`	—	—
`mul_comp` 📖	mathematical	—	`comp` `MulOne.toOne` `MulOneClass.toMulOne` `OneHom` `instMul`	—	—

ZeroHom

Definitions

Name	Category	Theorems
`instAdd` 📖	CompOp	6 math math: `instIsRightCancelAddZeroHom`, `instIsLeftCancelAddZeroHom`, `add_apply`, `instIsCancelAddZeroHom`, `coe_add`, `add_comp`
`instNeg` 📖	CompOp	3 math math: `neg_apply`, `neg_comp`, `coe_neg`
`instSub` 📖	CompOp	3 math math: `sub_comp`, `coe_sub`, `sub_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `AddZero.toZero` `AddZeroClass.toAddZero` `funLike` `instAdd` `AddZero.toAdd`	—	—
`add_comp` 📖	mathematical	—	`comp` `AddZero.toZero` `AddZeroClass.toAddZero` `ZeroHom` `instAdd`	—	—
`coe_add` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `AddZero.toZero` `AddZeroClass.toAddZero` `funLike` `instAdd` `Pi.instAdd` `AddZero.toAdd`	—	—
`coe_neg` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `NegZeroClass.toZero` `funLike` `instNeg` `Pi.instNeg` `NegZeroClass.toNeg`	—	—
`coe_sub` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `funLike` `instSub` `Pi.instSub` `SubNegMonoid.toSub` `SubtractionMonoid.toSubNegMonoid`	—	—
`neg_apply` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `NegZeroClass.toZero` `funLike` `instNeg` `NegZeroClass.toNeg`	—	—
`neg_comp` 📖	mathematical	—	`comp` `NegZeroClass.toZero` `ZeroHom` `instNeg`	—	—
`sub_apply` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `funLike` `instSub` `SubNegMonoid.toSub` `SubtractionMonoid.toSubNegMonoid`	—	—
`sub_comp` 📖	mathematical	—	`comp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `ZeroHom` `instSub`	—	—

(root)

Definitions

Name	Category	Theorems
`invMonoidHom` 📖	CompOp	4 math math: `invMonoidHom_apply`, `coe_invMonoidHom`, `IsMulIndecomposable.image_baseOf_inv_comp_eq`, `invMonoidHom_comp_invMonoidHom`
`negAddMonoidHom` 📖	CompOp	4 math math: `IsAddIndecomposable.image_baseOf_neg_comp_eq`, `negAddMonoidHom_apply`, `negAddMonoidHom_comp_negAddMonoidHom`, `coe_negAddMonoidHom`
`nsmulAddMonoidHom` 📖	CompOp	8 math math: `AddCircle.isAddQuotientCoveringMap_nsmul_of_ne_zero`, `AddCircle.isAddQuotientCoveringMap_nsmul`, `IsAddCyclic.index_nsmulAddMonoidHom_range`, `nsmulAddMonoidHom_apply`, `IsAddCyclic.card_nsmulAddMonoidHom_ker`, `DistribSMul.toAddMonoidHom_eq_nsmulAddMonoidHom`, `IsAddCyclic.index_nsmulAddMonoidHom_ker`, `IsAddCyclic.card_nsmulAddMonoidHom_range`
`powMonoidHom` 📖	CompOp	15 math math: `Complex.isQuotientCoveringMap_npow`, `IsDedekindDomain.selmerGroup.monotone`, `isQuotientCoveringMap_npow`, `IsCyclic.card_powMonoidHom_ker`, `rootsOfUnity_eq_ker`, `Circle.isQuotientCoveringMap_npow`, `IsCyclic.index_powMonoidHom_ker`, `IsCyclic.index_powMonoidHom_range`, `IsDedekindDomain.selmerGroup.fromUnit_ker`, `IsDedekindDomain.selmerGroup.fromUnitLift_injective`, `IsCyclic.card_powMonoidHom_range`, `IsDedekindDomain.HeightOneSpectrum.valuation_of_unit_mod_eq`, `powMonoidHom_apply`, `NumberField.IsCMField.map_unitsMulComplexConjInv_torsion`, `IsDedekindDomain.selmerGroup.valuation_ker_eq`
`zpowGroupHom` 📖	CompOp	10 math math: `QuotientGroup.homQuotientZPowOfHom_id`, `ker_zpowGroupHom_eq_rootsOfUnity`, `Circle.isQuotientCoveringMap_zpow`, `zpowGroupHom_apply`, `QuotientGroup.homQuotientZPowOfHom_comp_of_rightInverse`, `isQuotientCoveringMap_zpow`, `QuotientGroup.homQuotientZPowOfHom_comp`, `QuotientGroup.equivQuotientZPowOfEquiv_trans`, `QuotientGroup.equivQuotientZPowOfEquiv_refl`, `QuotientGroup.equivQuotientZPowOfEquiv_symm`
`zsmulAddGroupHom` 📖	CompOp	10 math math: `AddCircle.isAddQuotientCoveringMap_zsmul_of_ne_zero`, `QuotientAddGroup.equivQuotientZSMulOfEquiv_symm`, `QuotientAddGroup.equivQuotientZSMulOfEquiv_trans`, `QuotientAddGroup.homQuotientZSMulOfHom_comp_of_rightInverse`, `zsmulAddGroupHom_apply`, `DistribSMul.toAddMonoidHom_eq_zsmulAddGroupHom`, `QuotientAddGroup.equivQuotientZSMulOfEquiv_refl`, `AddCircle.isAddQuotientCoveringMap_zsmul`, `QuotientAddGroup.homQuotientZSMulOfHom_comp`, `QuotientAddGroup.homQuotientZSMulOfHom_id`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_invMonoidHom` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `DivisionCommMonoid.toDivisionMonoid` `MonoidHom.instFunLike` `invMonoidHom` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid`	—	—
`coe_negAddMonoidHom` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddMonoidHom.instFunLike` `negAddMonoidHom` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid`	—	—
`injective_iff_map_eq_one` 📖	mathematical	—	`DFunLike.coe` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`map_eq_one_iff` `MonoidHomClass.toOneHomClass` `mul_inv_eq_one` `map_mul` `MonoidHomClass.toMulHomClass` `mul_inv_cancel` `map_one`
`injective_iff_map_eq_one'` 📖	mathematical	—	`DFunLike.coe` `MulOne.toOne` `MulOneClass.toMulOne` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`injective_iff_map_eq_one` `map_one` `MonoidHomClass.toOneHomClass`
`injective_iff_map_eq_zero` 📖	mathematical	—	`DFunLike.coe` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`map_eq_zero_iff` `AddMonoidHomClass.toZeroHomClass` `add_neg_eq_zero` `map_add` `AddMonoidHomClass.toAddHomClass` `add_neg_cancel` `map_zero`
`injective_iff_map_eq_zero'` 📖	mathematical	—	`DFunLike.coe` `AddZero.toZero` `AddZeroClass.toAddZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`injective_iff_map_eq_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass`
`invMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `DivisionCommMonoid.toDivisionMonoid` `MonoidHom.instFunLike` `invMonoidHom` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid`	—	—
`invMonoidHom_comp_invMonoidHom` 📖	mathematical	—	`MonoidHom.comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `DivisionCommMonoid.toDivisionMonoid` `invMonoidHom` `MonoidHom.id`	—	`MonoidHom.ext` `inv_inv`
`negAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddMonoidHom.instFunLike` `negAddMonoidHom` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid`	—	—
`negAddMonoidHom_comp_negAddMonoidHom` 📖	mathematical	—	`AddMonoidHom.comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `negAddMonoidHom` `AddMonoidHom.id`	—	`AddMonoidHom.ext` `neg_neg`
`nsmulAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `nsmulAddMonoidHom` `AddMonoid.toNatSMul`	—	—
`powMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom.instFunLike` `powMonoidHom` `Monoid.toNatPow`	—	—
`zpowGroupHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `DivisionCommMonoid.toDivisionMonoid` `MonoidHom.instFunLike` `zpowGroupHom` `DivInvMonoid.toZPow`	—	—
`zsmulAddGroupHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddMonoidHom.instFunLike` `zsmulAddGroupHom` `SubNegMonoid.toZSMul`	—	—

---

← Back to Index