Documentation Verification Report

Instances

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

Statistics

Metric	Count
Definitions `instAddCommGroup`, `instAddCommMonoid`, `instIntCast`, `compHom`, `compHom'`, `compl₂`, `compr₂`, `eval`, `flip`, `flipHom`, `instAddCommGroup`, `instAddCommMonoid`, `instIntSMul`, `instNatSMul`, `compHom`, `compHom'`, `compl₂`, `compr₂`, `eval`, `flip`, `flipHom`, `instCommGroup`, `instCommMonoid`, `instIntPow`, `instPow`, `instCommGroup`, `instCommMonoid`, `instGroup`, `instIntPow`, `instMonoid`, `instPow`, `instAddCommGroup`, `instAddCommMonoid`, `instAddGroup`, `instAddMonoid`, `instIntSMul`, `instNatSMul`	37
Theorems `intCast_apply`, `one_apply`, `zero_apply`, `compHom'_apply_apply`, `compHom_apply_apply`, `compl₂_apply`, `compr₂_apply`, `eval_apply_apply`, `ext_iff₂`, `flipHom_apply`, `flip_apply`, `map_div₂`, `map_inv₂`, `map_mul₂`, `map_one₂`, `nsmul_apply`, `zsmul_apply`, `compHom'_apply_apply`, `compHom_apply_apply`, `compl₂_apply`, `compr₂_apply`, `eval_apply_apply`, `ext_iff₂`, `flipHom_apply`, `flip_apply`, `map_div₂`, `map_inv₂`, `map_mul₂`, `map_one₂`, `pow_apply`, `zpow_apply`, `pow_apply`, `zpow_apply`, `nsmul_apply`, `zsmul_apply`, `instIsCancelAddAddMonoidHom`, `instIsCancelAddZeroHom`, `instIsCancelMulMonoidHom`, `instIsCancelMulOneHom`, `instIsLeftCancelAddAddMonoidHom`, `instIsLeftCancelAddZeroHom`, `instIsLeftCancelMulMonoidHom`, `instIsLeftCancelMulOneHom`, `instIsRightCancelAddAddMonoidHom`, `instIsRightCancelAddZeroHom`, `instIsRightCancelMulMonoidHom`, `instIsRightCancelMulOneHom`	47
Total	84

AddMonoid.End

Definitions

Name	Category	Theorems
`instAddCommGroup` 📖	CompOp	1 math math: `CentroidHom.toEnd_neg`
`instAddCommMonoid` 📖	CompOp	13 math math: `mulRight_apply_apply`, `commute_lmul_rmul`, `CentroidHom.centroid_eq_centralizer_mulLeftRight`, `two_nsmul_lie_lmul_lmul_add_add_eq_zero`, `commute_lmul_sq_rmul`, `commute_lmul_rmul_sq`, `mulLeft_apply_apply`, `NonUnitalNonAssocCommSemiring.mem_center_iff`, `commute_lmul_lmul_sq`, `two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add`, `NonUnitalNonAssocSemiring.mem_center_iff`, `commute_rmul_rmul_sq`, `zero_apply`
`instIntCast` 📖	CompOp	3 math math: `intCast_apply`, `CentroidHom.toEnd_intCast`, `intCast_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`intCast_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoid.End` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instFunLike` `instIntCast` `SubNegMonoid.toZSMul`	—	—
`one_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoid.End` `AddZeroClass.toAddZero` `instFunLike` `instOne`	—	—
`zero_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoid.End` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `AddZero.toZero` `instAddCommMonoid`	—	—

AddMonoidHom

Definitions

Name	Category	Theorems
`compHom` 📖	CompOp	5 math math: `compHom_apply_apply`, `AddCommMonCat.coyoneda_map_app`, `AddCommGrpCat.coyoneda_map_app`, `AddCommMonCat.coyoneda_obj_map`, `AddCommGrpCat.coyoneda_obj_map`
`compHom'` 📖	CompOp	3 math math: `AddCommMonCat.coyoneda_map_app`, `compHom'_apply_apply`, `AddCommGrpCat.coyoneda_map_app`
`compl₂` 📖	CompOp	3 math math: `Set.mem_center_iff_addMonoidHom`, `compl₂_apply`, `map_mul_iff`
`compr₂` 📖	CompOp	3 math math: `Set.mem_center_iff_addMonoidHom`, `compr₂_apply`, `map_mul_iff`
`eval` 📖	CompOp	2 math math: `eval_apply_apply`, `dfinsuppSumAddHom_apply`
`flip` 📖	CompOp	5 math math: `coe_flip_mul`, `flip_apply`, `Finsupp.toFreeAbelianGroup_comp_singleAddHom`, `DFinsupp.sumAddHom_comm`, `flipHom_apply`
`flipHom` 📖	CompOp	1 math math: `flipHom_apply`
`instAddCommGroup` 📖	CompOp	18 math math: `groupCohomology.H1IsoOfIsTrivial_inv_apply`, `groupCohomology.cocycles₁IsoOfIsTrivial_hom_hom_apply_apply`, `Module.Free.addMonoidHom`, `LieRingModule.toEnd_apply_apply`, `groupCohomology.H1IsoOfIsTrivial_H1π_apply_apply`, `associator_apply`, `CategoryTheory.Abelian.Ext.bilinearComp_apply_apply`, `map_inv₂`, `Module.Finite.addMonoidHom`, `groupCohomology.cocycles₁IsoOfIsTrivial_inv_hom_apply_coe`, `groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom_apply`, `associator_eq_zero_iff_associative`, `map_div₂`, `AddCommGrpCat.coyoneda_map_app`, `associator_eq_zero`, `groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom`, `groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom_assoc`, `AddCommGrpCat.coyoneda_obj_map`
`instAddCommMonoid` 📖	CompOp	53 math math: `DirectSum.mulHom_of_of`, `DirectSum.Gmodule.smulAddMonoidHom_apply_of_of`, `addMonoidHomLequivNat_symm_apply`, `restrictHom_apply`, `addMonoidHomLequivInt_apply`, `DirectSum.fromAddMonoid_of_apply`, `coe_flip_mul`, `Set.mem_center_iff_addMonoidHom`, `coe_smul'`, `DirectSum.fromAddMonoid_of`, `DirectSum.gMulHom_apply_apply`, `coe_dfinsuppSumAddHom`, `eval_apply_apply`, `flip_apply`, `LinearMap.toAddMonoidHom'_apply`, `Module.Free.addMonoidHom`, `Finsupp.toFreeAbelianGroup_comp_singleAddHom`, `compl₂_apply`, `coe_finset_sum`, `DFinsupp.sumAddHom_comm`, `compr₂_apply`, `finsuppSum_apply`, `mulLeft₃_apply`, `mul_apply`, `compHom_apply_apply`, `addMonoidEndRingEquivInt_apply`, `AddCommMonCat.coyoneda_map_app`, `Module.Finite.addMonoidHom`, `compHom'_apply_apply`, `map_mul₂`, `DirectSum.mulHom_apply`, `dfinsuppSum_apply`, `smulAddHom_apply`, `coe_mul`, `addMonoidHomLequivNat_apply`, `addMonoidHomLequivInt_symm_apply`, `AddCommGrpCat.coyoneda_map_app`, `coeFn_apply`, `coe_dfinsuppSum`, `AddCommMonCat.coyoneda_obj_map`, `dfinsuppSumAddHom_apply`, `addMonoidEndRingEquivInt_symm_apply`, `finset_sum_apply`, `CharacterModule.homEquiv_apply_apply`, `map_one₂`, `DirectSum.gsmulHom_apply_apply`, `map_mul_iff`, `ext_iff₂`, `flipHom_apply`, `mulRight₃_apply`, `DirectSum.Gmodule.smul_def`, `coe_finsuppSum`, `AddCommGrpCat.coyoneda_obj_map`
`instIntSMul` 📖	CompOp	2 math math: `zsmul_apply`, `AddCommGrpCat.hom_zsmul`
`instNatSMul` 📖	CompOp	2 math math: `AddCommGrpCat.hom_nsmul`, `nsmul_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compHom'_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `instAddCommMonoid` `compHom'`	—	—
`compHom_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `instFunLike` `compHom` `comp`	—	—
`compl₂_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `instAddCommMonoid` `compl₂`	—	—
`compr₂_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `instAddCommMonoid` `compr₂`	—	—
`eval_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `instFunLike` `eval`	—	—
`ext_iff₂` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `instAddCommMonoid`	—	`DFunLike.ext_iff`
`flipHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `instFunLike` `flipHom` `flip`	—	—
`flip_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `instAddCommMonoid` `flip`	—	—
`map_div₂` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instFunLike` `instAddCommGroup` `SubNegMonoid.toSub`	—	`map_sub`
`map_inv₂` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instFunLike` `instAddCommGroup` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`map_neg`
`map_mul₂` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `instAddCommMonoid` `AddZero.toAdd`	—	`map_add`
`map_one₂` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `instAddCommMonoid` `AddZero.toZero`	—	`map_zero`
`nsmul_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `instNatSMul` `AddMonoid.toNatSMul`	—	—
`zsmul_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instFunLike` `instIntSMul` `SubNegMonoid.toZSMul`	—	—

MonoidHom

Definitions

Name	Category	Theorems
`compHom` 📖	CompOp	5 math math: `compHom_apply_apply`, `CommMonCat.coyoneda_obj_map`, `CommMonCat.coyoneda_map_app`, `CommGrpCat.coyoneda_obj_map`, `CommGrpCat.coyoneda_map_app`
`compHom'` 📖	CompOp	3 math math: `compHom'_apply_apply`, `CommMonCat.coyoneda_map_app`, `CommGrpCat.coyoneda_map_app`
`compl₂` 📖	CompOp	1 math math: `compl₂_apply`
`compr₂` 📖	CompOp	1 math math: `compr₂_apply`
`eval` 📖	CompOp	1 math math: `eval_apply_apply`
`flip` 📖	CompOp	2 math math: `flip_apply`, `flipHom_apply`
`flipHom` 📖	CompOp	1 math math: `flipHom_apply`
`instCommGroup` 📖	CompOp	6 math math: `restrictHomKerEquiv_apply_coe`, `map_div₂`, `restrictHomKerEquiv_symm_coe_apply`, `map_inv₂`, `CommGrpCat.coyoneda_obj_map`, `CommGrpCat.coyoneda_map_app`
`instCommMonoid` 📖	CompOp	23 math math: `map_mul₂`, `finset_prod_apply`, `compHom_apply_apply`, `CommMonCat.coyoneda_obj_map`, `coeFn_apply`, `map_one₂`, `coe_finsuppProd`, `compHom'_apply_apply`, `finsuppProd_apply`, `restrictHom_apply`, `CommMonCat.coyoneda_map_app`, `coe_dfinsuppProd`, `eval_apply_apply`, `ext_iff₂`, `restrict_surjective`, `dfinsuppProd_apply`, `CommGrpCat.coyoneda_obj_map`, `compr₂_apply`, `flip_apply`, `coe_finset_prod`, `flipHom_apply`, `CommGrpCat.coyoneda_map_app`, `compl₂_apply`
`instIntPow` 📖	CompOp	1 math math: `zpow_apply`
`instPow` 📖	CompOp	1 math math: `pow_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compHom'_apply_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instFunLike` `instCommMonoid` `compHom'`	—	—
`compHom_apply_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instCommMonoid` `instFunLike` `compHom` `comp`	—	—
`compl₂_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instFunLike` `instCommMonoid` `compl₂`	—	—
`compr₂_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instFunLike` `instCommMonoid` `compr₂`	—	—
`eval_apply_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instCommMonoid` `instFunLike` `eval`	—	—
`ext_iff₂` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instFunLike` `instCommMonoid`	—	`DFunLike.ext_iff`
`flipHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instCommMonoid` `instFunLike` `flipHom` `flip`	—	—
`flip_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instFunLike` `instCommMonoid` `flip`	—	—
`map_div₂` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instFunLike` `instCommGroup` `DivInvMonoid.toDiv`	—	`map_div`
`map_inv₂` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instFunLike` `instCommGroup` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	—	`map_inv`
`map_mul₂` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instFunLike` `instCommMonoid` `MulOne.toMul`	—	`map_mul`
`map_one₂` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instFunLike` `instCommMonoid` `MulOne.toOne`	—	`map_one`
`pow_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instFunLike` `instPow` `Monoid.toNatPow`	—	—
`zpow_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instFunLike` `instIntPow` `DivInvMonoid.toZPow`	—	—

OneHom

Definitions

Name	Category	Theorems
`instCommGroup` 📖	CompOp	—
`instCommMonoid` 📖	CompOp	—
`instGroup` 📖	CompOp	—
`instIntPow` 📖	CompOp	1 math math: `zpow_apply`
`instMonoid` 📖	CompOp	—
`instPow` 📖	CompOp	1 math math: `pow_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pow_apply` 📖	mathematical	—	`DFunLike.coe` `OneHom` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `funLike` `instPow` `Monoid.toNatPow`	—	—
`zpow_apply` 📖	mathematical	—	`DFunLike.coe` `OneHom` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `funLike` `instIntPow` `DivInvMonoid.toZPow` `Group.toDivInvMonoid`	—	—

ZeroHom

Definitions

Name	Category	Theorems
`instAddCommGroup` 📖	CompOp	—
`instAddCommMonoid` 📖	CompOp	—
`instAddGroup` 📖	CompOp	—
`instAddMonoid` 📖	CompOp	—
`instIntSMul` 📖	CompOp	1 math math: `zsmul_apply`
`instNatSMul` 📖	CompOp	1 math math: `nsmul_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nsmul_apply` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `funLike` `instNatSMul` `AddMonoid.toNatSMul`	—	—
`zsmul_apply` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `funLike` `instIntSMul` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid`	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsCancelAddAddMonoidHom` 📖	mathematical	—	`IsCancelAdd` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.add`	—	`instIsLeftCancelAddAddMonoidHom` `IsCancelAdd.toIsLeftCancelAdd` `instIsRightCancelAddAddMonoidHom` `IsCancelAdd.toIsRightCancelAdd`
`instIsCancelAddZeroHom` 📖	mathematical	—	`IsCancelAdd` `ZeroHom` `AddZero.toZero` `AddZeroClass.toAddZero` `ZeroHom.instAdd`	—	`instIsLeftCancelAddZeroHom` `IsCancelAdd.toIsLeftCancelAdd` `instIsRightCancelAddZeroHom` `IsCancelAdd.toIsRightCancelAdd`
`instIsCancelMulMonoidHom` 📖	mathematical	—	`IsCancelMul` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom.mul`	—	`instIsLeftCancelMulMonoidHom` `IsCancelMul.toIsLeftCancelMul` `instIsRightCancelMulMonoidHom` `IsCancelMul.toIsRightCancelMul`
`instIsCancelMulOneHom` 📖	mathematical	—	`IsCancelMul` `OneHom` `MulOne.toOne` `MulOneClass.toMulOne` `OneHom.instMul`	—	`instIsLeftCancelMulOneHom` `IsCancelMul.toIsLeftCancelMul` `instIsRightCancelMulOneHom` `IsCancelMul.toIsRightCancelMul`
`instIsLeftCancelAddAddMonoidHom` 📖	mathematical	—	`IsLeftCancelAdd` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.add`	—	`Function.Injective.isLeftCancelAdd` `Pi.instIsLeftCancelAdd` `DFunLike.coe_injective`
`instIsLeftCancelAddZeroHom` 📖	mathematical	—	`IsLeftCancelAdd` `ZeroHom` `AddZero.toZero` `AddZeroClass.toAddZero` `ZeroHom.instAdd`	—	`Function.Injective.isLeftCancelAdd` `Pi.instIsLeftCancelAdd` `DFunLike.coe_injective`
`instIsLeftCancelMulMonoidHom` 📖	mathematical	—	`IsLeftCancelMul` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom.mul`	—	`Function.Injective.isLeftCancelMul` `Pi.instIsLeftCancelMul` `DFunLike.coe_injective`
`instIsLeftCancelMulOneHom` 📖	mathematical	—	`IsLeftCancelMul` `OneHom` `MulOne.toOne` `MulOneClass.toMulOne` `OneHom.instMul`	—	`Function.Injective.isLeftCancelMul` `Pi.instIsLeftCancelMul` `DFunLike.coe_injective`
`instIsRightCancelAddAddMonoidHom` 📖	mathematical	—	`IsRightCancelAdd` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.add`	—	`Function.Injective.isRightCancelAdd` `Pi.instIsRightCancelAdd` `DFunLike.coe_injective`
`instIsRightCancelAddZeroHom` 📖	mathematical	—	`IsRightCancelAdd` `ZeroHom` `AddZero.toZero` `AddZeroClass.toAddZero` `ZeroHom.instAdd`	—	`Function.Injective.isRightCancelAdd` `Pi.instIsRightCancelAdd` `DFunLike.coe_injective`
`instIsRightCancelMulMonoidHom` 📖	mathematical	—	`IsRightCancelMul` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom.mul`	—	`Function.Injective.isRightCancelMul` `Pi.instIsRightCancelMul` `DFunLike.coe_injective`
`instIsRightCancelMulOneHom` 📖	mathematical	—	`IsRightCancelMul` `OneHom` `MulOne.toOne` `MulOneClass.toMulOne` `OneHom.instMul`	—	`Function.Injective.isRightCancelMul` `Pi.instIsRightCancelMul` `DFunLike.coe_injective`

---

← Back to Index