AddChar

📁 Source: Mathlib/Algebra/Group/AddChar.lean

Statistics

Metric	Count
Definitions `compAddMonoidHom`, `doubleDualEmb`, `instAddCommGroup`, `instAddCommMonoid`, `instCommGroup`, `instCommMonoid`, `instDecidableEq`, `instFunLike`, `instInhabited`, `instOne`, `instZero`, `mulShift`, `toAddMonoidAddEquiv`, `toAddMonoidHom`, `toAddMonoidHomEquiv`, `toFun`, `toMonoidHom`, `toMonoidHomEquiv`, `toMonoidHomMulEquiv`, `compAddChar`	20
Theorems `add_apply`, `coe_add`, `coe_compAddMonoidHom`, `coe_eq_one`, `coe_mk`, `coe_mul`, `coe_ne_zero`, `coe_nsmul`, `coe_one`, `coe_pow`, `coe_prod`, `coe_sum`, `coe_toAddMonoidHom`, `coe_toAddMonoidHomEquiv`, `coe_toAddMonoidHomEquiv_symm`, `coe_toMonoidHomEquiv`, `coe_toMonoidHomEquiv_symm`, `coe_zero`, `compAddMonoidHom_apply`, `compAddMonoidHom_injective_left`, `compAddMonoidHom_injective_right`, `div_apply`, `div_apply'`, `doubleDualEmb_apply`, `eq_one_iff`, `eq_zero_iff`, `ext`, `ext_iff`, `injective_iff`, `inv_apply`, `inv_apply'`, `inv_mulShift`, `map_add_eq_mul`, `map_add_eq_mul'`, `map_neg_eq_inv`, `map_nsmul_eq_pow`, `map_sub_eq_div`, `map_zero_eq_one`, `map_zero_eq_one'`, `map_zsmul_eq_zpow`, `mulShift_apply`, `mulShift_mul`, `mulShift_mulShift`, `mulShift_one`, `mulShift_spec'`, `mulShift_unit_eq_one_iff`, `mulShift_zero`, `mul_apply`, `mul_eq_add`, `ne_one_iff`, `ne_zero_iff`, `neg_apply`, `neg_apply'`, `nsmul_apply`, `one_apply`, `one_eq_zero`, `pow_apply`, `pow_eq_nsmul`, `pow_mulShift`, `prod_apply`, `prod_eq_sum`, `sub_apply`, `sub_apply'`, `sum_apply`, `sum_eq_ite`, `sum_eq_zero_iff_ne_zero`, `sum_ne_zero_iff_eq_zero`, `toAddMonoidHomEquiv_apply`, `toAddMonoidHomEquiv_symm_apply`, `toAddMonoidHomEquiv_symm_zero`, `toAddMonoidHomEquiv_zero`, `toAddMonoidHom_apply`, `toMonoidHomEquiv_add`, `toMonoidHomEquiv_apply`, `toMonoidHomEquiv_symm_apply`, `toMonoidHomEquiv_symm_mul`, `toMonoidHomEquiv_symm_one`, `toMonoidHomEquiv_zero`, `toMonoidHom_apply`, `val_isUnit`, `zero_apply`, `zpow_apply`, `zsmul_apply`, `coe_compAddChar`, `compAddChar_apply`, `compAddChar_injective_left`, `compAddChar_injective_right`	87
Total	107

AddChar

Definitions

Name	Category	Theorems
`compAddMonoidHom` 📖	CompOp	4 math math: `compAddMonoidHom_injective_left`, `coe_compAddMonoidHom`, `compAddMonoidHom_apply`, `compAddMonoidHom_injective_right`
`doubleDualEmb` 📖	CompOp	8 math math: `doubleDualEmb_injective`, `doubleDualEmb_apply`, `doubleDualEmb_bijective`, `coe_doubleDualEquiv`, `doubleDualEquiv_symm_doubleDualEmb_apply`, `doubleDualEmb_inj`, `doubleDualEmb_eq_zero`, `doubleDualEmb_doubleDualEquiv_symm_apply`
`instAddCommGroup` 📖	CompOp	8 math math: `sub_apply`, `neg_apply`, `neg_apply'`, `zsmul_apply`, `coe_doubleDualEquiv`, `doubleDualEquiv_symm_doubleDualEmb_apply`, `doubleDualEmb_doubleDualEquiv_symm_apply`, `sub_apply'`
`instAddCommMonoid` 📖	CompOp	20 math math: `mul_eq_add`, `doubleDualEmb_injective`, `add_apply`, `sum_apply`, `doubleDualEmb_apply`, `doubleDualEmb_bijective`, `coe_doubleDualEquiv`, `toMonoidHomEquiv_add`, `pow_eq_nsmul`, `prod_eq_sum`, `coe_add`, `toMonoidHomEquiv_symm_mul`, `doubleDualEquiv_symm_doubleDualEmb_apply`, `doubleDualEmb_inj`, `doubleDualEmb_eq_zero`, `doubleDualEmb_doubleDualEquiv_symm_apply`, `coe_nsmul`, `zmodAddEquiv_apply`, `nsmul_apply`, `coe_sum`
`instCommGroup` 📖	CompOp	14 math math: `zmod_add`, `gaussSum_frob`, `mul_gaussSum_inv_eq_gaussSum`, `pow_mulShift`, `div_apply`, `inv_apply`, `mulShift_mul`, `inv_apply'`, `starComp_apply`, `starComp_eq_inv`, `gaussSum_mul_gaussSum_eq_card`, `zpow_apply`, `div_apply'`, `inv_mulShift`
`instCommMonoid` 📖	CompOp	9 math math: `mul_eq_add`, `coe_mul`, `prod_apply`, `pow_apply`, `coe_pow`, `mul_apply`, `pow_eq_nsmul`, `prod_eq_sum`, `coe_prod`
`instDecidableEq` 📖	CompOp	2 math math: `wInner_cWeight_eq_boole`, `expect_eq_ite`
`instFunLike` 📖	CompOp	159 math math: `Polynomial.rightInverse_ofMultiset_roots`, `Real.hasFDerivAt_fourierChar_neg_bilinear_left`, `AddDissociated.randomisation`, `ZMod.LFunction_stdAddChar_eq_expZeta`, `Subgroup.HasDetPlusMinusOne.isParabolic_iff_of_upperTriangular`, `map_nsmul_eq_pow`, `Real.fourierIntegral_eq`, `Real.fderiv_fourierChar_neg_bilinear_right_apply`, `ZMod.invDFT_apply`, `wInner_cWeight_self`, `sum_mulShift`, `coe_mul`, `Circle.starRingEnd_addChar`, `prod_apply`, `add_apply`, `directSum_apply`, `tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support`, `ZMod.stdAddChar_coe`, `zero_apply`, `IsPrimitive.zmod_char_eq_one_iff`, `sum_eq_ite`, `sub_apply`, `map_neg_eq_inv`, `map_zsmul_eq_zpow`, `gaussSum_mul`, `neg_apply`, `sum_apply`, `coe_compAddMonoidHom`, `wInner_cWeight_eq_zero_iff_ne`, `sum_apply_eq_ite`, `toMonoidHomEquiv_symm_apply`, `ext_iff`, `sum_eq_zero_iff_ne_zero`, `Matrix.GeneralLinearGroup.upperRightHom_apply`, `sum_eq_card_of_eq_one`, `coe_toMonoidHomEquiv`, `tendsto_integral_exp_smul_cocompact`, `map_add_eq_mul`, `PadicInt.coe_addChar_of_value_at_one`, `pow_apply`, `Real.fourier_real_eq`, `Real.fourierIntegral_convergent_iff'`, `expect_apply_eq_zero_iff_ne_zero`, `doubleDualEmb_apply`, `forall_apply_eq_zero`, `Real.continuous_probChar`, `sum_apply_eq_zero_iff_ne_zero`, `coe_toAddMonoidHom`, `neg_apply'`, `zsmul_apply`, `map_zero_eq_one`, `zmodChar_apply'`, `Matrix.GeneralLinearGroup.isParabolic_iff_of_upperTriangular_of_det`, `fourierIntegral_eq_half_sub_half_period_translate`, `div_apply`, `Matrix.GeneralLinearGroup.continuous_upperRightHom`, `coe_pow`, `mulShift_apply`, `coe_toAddMonoidHomEquiv`, `toMonoidHom_apply`, `sum_eq_zero_of_ne_one`, `Circle.star_addChar`, `inv_apply`, `wInner_cWeight_eq_one_iff_eq`, `ZMod.dft_apply`, `val_mem_rootsOfUnity`, `bijective_rootsOfUnityAddChar`, `one_apply`, `Real.fourier_eq`, `expect_eq_zero_iff_ne_zero`, `tendsto_integral_exp_smul_cocompact_of_inner_product`, `toAddMonoidHomEquiv_symm_apply`, `surjective_rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar`, `inv_apply'`, `Polynomial.roots_ofMultiset`, `val_isUnit`, `mulShift_spec'`, `zmodChar_apply`, `starComp_apply`, `PadicInt.continuous_addChar_of_value_at_one`, `mul_apply`, `coe_zero`, `PadicInt.continuousAddCharEquiv_of_norm_mul_symm_apply`, `eq_zero_iff`, `toMonoidHomEquiv_apply`, `norm_apply`, `Real.probChar_apply'`, `MonoidHom.coe_compAddChar`, `Polynomial.ofMultiset_apply`, `Real.fourierIntegral_convergent_iff`, `Real.hasDerivAt_fourierChar`, `compAddMonoidHom_apply`, `Real.fourierChar_apply`, `Real.fourier_bilin_convolution_eq_integral`, `Real.tendsto_integral_exp_smul_cocompact`, `fourierIntegral_half_period_translate`, `coe_prod`, `toAddMonoidHom_apply`, `coe_add`, `Real.fourierChar_apply'`, `Real.differentiable_fourierChar`, `Real.continuous_fourierChar`, `Subgroup.mem_strictPeriods_iff`, `rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar_val`, `ZMod.toCircle_intCast`, `ZMod.toCircle_natCast`, `Real.deriv_fourierChar`, `ZMod.invDFT_def`, `Real.differentiable_fourierChar_neg_bilinear_right`, `ZMod.injective_toCircle`, `VectorFourier.fourierIntegral_comp_add_right`, `tendsto_integral_exp_inner_smul_cocompact`, `Fourier.fourierIntegral_def`, `PadicInt.continuousAddCharEquiv_symm_apply`, `linearIndependent`, `Real.hasFDerivAt_fourierChar_neg_bilinear_right`, `ZMod.toCircle_apply`, `fwdDiff_addChar_eq`, `Real.differentiable_fourierChar_neg_bilinear_left`, `wInner_cWeight_eq_boole`, `map_neg_eq_conj`, `coe_complexBasis`, `Real.fourierInv_eq`, `toAddMonoidHomEquiv_apply`, `MonoidHom.compAddChar_apply`, `map_sub_eq_div`, `complexBasis_apply`, `coe_nsmul`, `Polynomial.ofMultiset_injective`, `Real.probChar_apply`, `injective_iff`, `zmod_intCast`, `coe_eq_one`, `expect_apply_eq_ite`, `Matrix.GeneralLinearGroup.injective_upperRightHom`, `VectorFourier.hasFDerivAt_fourierChar_smul`, `Real.fourierIntegral_real_eq`, `ZMod.injective_stdAddChar`, `coe_one`, `Real.fourierIntegralInv_eq`, `zpow_apply`, `Real.fderiv_fourierChar_neg_bilinear_left_apply`, `ZMod.dft_def`, `eq_one_iff`, `Fourier.fourierIntegral_comp_add_right`, `inv_apply_eq_conj`, `nsmul_apply`, `div_apply'`, `sub_apply'`, `ZMod.rootsOfUnityAddChar_val`, `ZMod.toCircle_eq_circleExp`, `ZMod.stdAddChar_apply`, `coe_mk`, `expect_eq_ite`, `MeasureTheory.charFun_eq_integral_probChar`, `coe_toMonoidHomEquiv_symm`, `coe_toAddMonoidHomEquiv_symm`, `PadicInt.addChar_of_value_at_one_def`, `coe_sum`
`instInhabited` 📖	CompOp	—
`instOne` 📖	CompOp	8 math math: `exists_divisor_of_not_isPrimitive`, `mulShift_unit_eq_one_iff`, `one_apply`, `one_eq_zero`, `mulShift_zero`, `zmod_zero`, `coe_one`, `eq_one_iff`
`instZero` 📖	CompOp	14 math math: `toMonoidHomEquiv_zero`, `expect_ne_zero_iff_eq_zero`, `zero_apply`, `sum_eq_ite`, `sum_ne_zero_iff_eq_zero`, `toAddMonoidHomEquiv_symm_zero`, `toMonoidHomEquiv_symm_one`, `one_eq_zero`, `coe_zero`, `eq_zero_iff`, `toAddMonoidHomEquiv_zero`, `doubleDualEmb_eq_zero`, `coe_eq_one`, `expect_eq_ite`
`mulShift` 📖	CompOp	15 math math: `mulShift_one`, `exists_divisor_of_not_isPrimitive`, `mulShift_unit_eq_one_iff`, `pow_mulShift`, `to_mulShift_inj_of_isPrimitive`, `mulShift_apply`, `gaussSum_mulShift_of_isPrimitive`, `mulShift_mul`, `mulShift_spec'`, `mulShift_zero`, `DirichletCharacter.fourierTransform_eq_gaussSum_mulShift`, `not_isPrimitive_mulShift`, `mulShift_mulShift`, `inv_mulShift`, `gaussSum_mulShift`
`toAddMonoidAddEquiv` 📖	CompOp	—
`toAddMonoidHom` 📖	CompOp	2 math math: `coe_toAddMonoidHom`, `toAddMonoidHom_apply`
`toAddMonoidHomEquiv` 📖	CompOp	7 math math: `directSum_apply`, `coe_toAddMonoidHomEquiv`, `toAddMonoidHomEquiv_symm_zero`, `toAddMonoidHomEquiv_symm_apply`, `toAddMonoidHomEquiv_zero`, `toAddMonoidHomEquiv_apply`, `coe_toAddMonoidHomEquiv_symm`
`toFun` 📖	CompOp	2 math math: `map_zero_eq_one'`, `map_add_eq_mul'`
`toMonoidHom` 📖	CompOp	1 math math: `toMonoidHom_apply`
`toMonoidHomEquiv` 📖	CompOp	8 math math: `toMonoidHomEquiv_zero`, `toMonoidHomEquiv_symm_apply`, `coe_toMonoidHomEquiv`, `toMonoidHomEquiv_symm_one`, `toMonoidHomEquiv_apply`, `toMonoidHomEquiv_add`, `toMonoidHomEquiv_symm_mul`, `coe_toMonoidHomEquiv_symm`
`toMonoidHomMulEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`DFunLike.coe` `AddChar` `CommMonoid.toMonoid` `instFunLike` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—
`coe_add` 📖	mathematical	—	`DFunLike.coe` `AddChar` `CommMonoid.toMonoid` `instFunLike` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoid` `Pi.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—
`coe_compAddMonoidHom` 📖	mathematical	—	`DFunLike.coe` `AddChar` `instFunLike` `compAddMonoidHom` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike`	—	—
`coe_eq_one` 📖	mathematical	—	`DFunLike.coe` `AddChar` `instFunLike` `Pi.instOne` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instZero`	—	`coe_zero` `DFunLike.coe_fn_eq`
`coe_mk` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `MulOne.toMul`	`DFunLike.coe` `AddChar` `instFunLike`	—	—
`coe_mul` 📖	mathematical	—	`DFunLike.coe` `AddChar` `CommMonoid.toMonoid` `instFunLike` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instCommMonoid` `Pi.instMul`	—	—
`coe_ne_zero` 📖	—	—	—	—	`Function.ne_iff` `NeZero.one` `map_zero_eq_one`
`coe_nsmul` 📖	mathematical	—	`DFunLike.coe` `AddChar` `CommMonoid.toMonoid` `instFunLike` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `Pi.instPow` `Monoid.toNatPow`	—	—
`coe_one` 📖	mathematical	—	`DFunLike.coe` `AddChar` `instFunLike` `instOne` `Pi.instOne` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—
`coe_pow` 📖	mathematical	—	`DFunLike.coe` `AddChar` `CommMonoid.toMonoid` `instFunLike` `Monoid.toNatPow` `instCommMonoid` `Pi.instPow`	—	—
`coe_prod` 📖	mathematical	—	`DFunLike.coe` `AddChar` `CommMonoid.toMonoid` `instFunLike` `Finset.prod` `instCommMonoid` `Pi.commMonoid`	—	`Finset.cons_induction` `Finset.prod_cons`
`coe_sum` 📖	mathematical	—	`DFunLike.coe` `AddChar` `CommMonoid.toMonoid` `instFunLike` `Finset.sum` `instAddCommMonoid` `Finset.prod` `Pi.commMonoid`	—	`Finset.cons_induction` `Finset.sum_cons` `Finset.prod_cons`
`coe_toAddMonoidHom` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Additive` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Additive.addZeroClass` `Monoid.toMulOneClass` `AddMonoidHom.instFunLike` `toAddMonoidHom` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Additive.ofMul` `AddChar` `instFunLike`	—	—
`coe_toAddMonoidHomEquiv` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Additive` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Additive.addZeroClass` `Monoid.toMulOneClass` `AddMonoidHom.instFunLike` `Equiv` `AddChar` `EquivLike.toFunLike` `Equiv.instEquivLike` `toAddMonoidHomEquiv` `Additive.ofMul` `instFunLike`	—	—
`coe_toAddMonoidHomEquiv_symm` 📖	mathematical	—	`DFunLike.coe` `AddChar` `instFunLike` `Equiv` `AddMonoidHom` `Additive` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Additive.addZeroClass` `Monoid.toMulOneClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toAddMonoidHomEquiv` `Additive.toMul` `AddMonoidHom.instFunLike`	—	—
`coe_toMonoidHomEquiv` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `Equiv` `AddChar` `EquivLike.toFunLike` `Equiv.instEquivLike` `toMonoidHomEquiv` `instFunLike` `Multiplicative.toAdd`	—	—
`coe_toMonoidHomEquiv_symm` 📖	mathematical	—	`DFunLike.coe` `AddChar` `instFunLike` `Equiv` `MonoidHom` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Monoid.toMulOneClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toMonoidHomEquiv` `MonoidHom.instFunLike` `Multiplicative.ofAdd`	—	—
`coe_zero` 📖	mathematical	—	`DFunLike.coe` `AddChar` `instFunLike` `instZero` `Pi.instOne` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—
`compAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddChar` `instFunLike` `compAddMonoidHom` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike`	—	—
`compAddMonoidHom_injective_left` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike`	`AddChar` `compAddMonoidHom`	—	`DFunLike.ext'_iff` `Function.Surjective.injective_comp_right`
`compAddMonoidHom_injective_right` 📖	mathematical	`DFunLike.coe` `AddChar` `instFunLike`	`AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `compAddMonoidHom`	—	`DFunLike.ext'_iff` `Function.Injective.comp_left`
`div_apply` 📖	mathematical	—	`DFunLike.coe` `AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CommMonoid.toMonoid` `instFunLike` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`div_apply'` 📖	mathematical	—	`DFunLike.coe` `AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `DivisionCommMonoid.toDivisionMonoid` `instFunLike` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroup` `DivisionCommMonoid.toCommMonoid`	—	`div_apply` `map_neg_eq_inv` `div_eq_mul_inv`
`doubleDualEmb_apply` 📖	mathematical	—	`DFunLike.coe` `AddChar` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `instFunLike` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `doubleDualEmb`	—	—
`eq_one_iff` 📖	mathematical	—	`AddChar` `instOne` `DFunLike.coe` `instFunLike` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`DFunLike.ext_iff`
`eq_zero_iff` 📖	mathematical	—	`AddChar` `instZero` `DFunLike.coe` `instFunLike` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`DFunLike.ext_iff`
`ext` 📖	—	`DFunLike.coe` `AddChar` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `AddChar` `instFunLike`	—	`ext`
`injective_iff` 📖	mathematical	—	`DFunLike.coe` `AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `DivisionCommMonoid.toDivisionMonoid` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`MonoidHom.ker_eq_bot_iff` `eq_bot_iff`
`inv_apply` 📖	mathematical	—	`DFunLike.coe` `AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CommMonoid.toMonoid` `instFunLike` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `instCommGroup` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`inv_apply'` 📖	mathematical	—	`DFunLike.coe` `AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `DivisionCommMonoid.toDivisionMonoid` `instFunLike` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `CommGroup.toDivisionCommMonoid` `instCommGroup` `DivisionCommMonoid.toCommMonoid`	—	`inv_apply` `map_neg_eq_inv`
`inv_mulShift` 📖	mathematical	—	`AddChar` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommMonoid.toMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `instCommGroup` `Ring.toAddCommGroup` `mulShift` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddMonoidWithOne.toOne`	—	`ext` `inv_apply` `mulShift_apply` `neg_mul` `one_mul`
`map_add_eq_mul` 📖	mathematical	—	`DFunLike.coe` `AddChar` `instFunLike` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`map_add_eq_mul'`
`map_add_eq_mul'` 📖	mathematical	—	`toFun` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—
`map_neg_eq_inv` 📖	mathematical	—	`DFunLike.coe` `AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `instFunLike` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid`	—	`eq_inv_of_mul_eq_one_left` `neg_add_cancel` `map_zero_eq_one`
`map_nsmul_eq_pow` 📖	mathematical	—	`DFunLike.coe` `AddChar` `instFunLike` `AddMonoid.toNatSMul` `Monoid.toNatPow`	—	`MonoidHom.map_pow`
`map_sub_eq_div` 📖	mathematical	—	`DFunLike.coe` `AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `DivisionCommMonoid.toDivisionMonoid` `instFunLike` `SubNegMonoid.toSub` `DivInvMonoid.toDiv`	—	`MonoidHom.map_div`
`map_zero_eq_one` 📖	mathematical	—	`DFunLike.coe` `AddChar` `instFunLike` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`map_zero_eq_one'`
`map_zero_eq_one'` 📖	mathematical	—	`toFun` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—
`map_zsmul_eq_zpow` 📖	mathematical	—	`DFunLike.coe` `AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `instFunLike` `SubNegMonoid.toZSMul` `DivInvMonoid.toZPow`	—	`MonoidHom.map_zpow`
`mulShift_apply` 📖	mathematical	—	`DFunLike.coe` `AddChar` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommMonoid.toMonoid` `instFunLike` `mulShift` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—
`mulShift_mul` 📖	mathematical	—	`AddChar` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroup` `Ring.toAddCommGroup` `mulShift` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`ext` `mulShift_apply` `right_distrib` `Distrib.rightDistribClass` `map_add_eq_mul`
`mulShift_mulShift` 📖	mathematical	—	`mulShift` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`ext` `mul_assoc`
`mulShift_one` 📖	mathematical	—	`mulShift` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`ext` `mulShift_apply` `one_mul`
`mulShift_spec'` 📖	mathematical	—	`DFunLike.coe` `AddChar` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommMonoid.toMonoid` `instFunLike` `mulShift` `AddMonoidWithOne.toNatCast` `Monoid.toNatPow`	—	`mulShift_apply` `nsmul_eq_mul` `map_nsmul_eq_pow`
`mulShift_unit_eq_one_iff` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	`mulShift` `AddChar` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommMonoid.toMonoid` `instOne`	—	`ext` `mul_assoc` `IsUnit.mul_val_inv` `one_mul` `DFunLike.ext_iff`
`mulShift_zero` 📖	mathematical	—	`mulShift` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddChar` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommMonoid.toMonoid` `instOne`	—	`ext` `mulShift_apply` `MulZeroClass.zero_mul` `map_zero_eq_one` `one_apply`
`mul_apply` 📖	mathematical	—	`DFunLike.coe` `AddChar` `CommMonoid.toMonoid` `instFunLike` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instCommMonoid`	—	—
`mul_eq_add` 📖	mathematical	—	`AddChar` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instCommMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoid`	—	—
`ne_one_iff` 📖	—	—	—	—	`DFunLike.ne_iff`
`ne_zero_iff` 📖	—	—	—	—	`DFunLike.ne_iff`
`neg_apply` 📖	mathematical	—	`DFunLike.coe` `AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CommMonoid.toMonoid` `instFunLike` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroup`	—	—
`neg_apply'` 📖	mathematical	—	`DFunLike.coe` `AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `DivisionCommMonoid.toDivisionMonoid` `instFunLike` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroup` `DivisionCommMonoid.toCommMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid`	—	`map_neg_eq_inv`
`nsmul_apply` 📖	mathematical	—	`DFunLike.coe` `AddChar` `CommMonoid.toMonoid` `instFunLike` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `Monoid.toNatPow`	—	—
`one_apply` 📖	mathematical	—	`DFunLike.coe` `AddChar` `instFunLike` `instOne` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—
`one_eq_zero` 📖	mathematical	—	`AddChar` `instOne` `instZero`	—	—
`pow_apply` 📖	mathematical	—	`DFunLike.coe` `AddChar` `CommMonoid.toMonoid` `instFunLike` `Monoid.toNatPow` `instCommMonoid`	—	—
`pow_eq_nsmul` 📖	mathematical	—	`AddChar` `CommMonoid.toMonoid` `Monoid.toNatPow` `instCommMonoid` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `instAddCommMonoid`	—	—
`pow_mulShift` 📖	mathematical	—	`AddChar` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommMonoid.toMonoid` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroup` `Ring.toAddCommGroup` `mulShift` `AddMonoidWithOne.toNatCast`	—	`ext` `pow_apply` `mulShift_spec'`
`prod_apply` 📖	mathematical	—	`DFunLike.coe` `AddChar` `CommMonoid.toMonoid` `instFunLike` `Finset.prod` `instCommMonoid`	—	`coe_prod` `Finset.prod_apply`
`prod_eq_sum` 📖	mathematical	—	`Finset.prod` `AddChar` `CommMonoid.toMonoid` `instCommMonoid` `Finset.sum` `instAddCommMonoid`	—	—
`sub_apply` 📖	mathematical	—	`DFunLike.coe` `AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CommMonoid.toMonoid` `instFunLike` `SubNegMonoid.toSub` `instAddCommGroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`sub_apply'` 📖	mathematical	—	`DFunLike.coe` `AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `DivisionCommMonoid.toDivisionMonoid` `instFunLike` `SubNegMonoid.toSub` `instAddCommGroup` `DivisionCommMonoid.toCommMonoid` `DivInvMonoid.toDiv`	—	`sub_apply` `map_neg_eq_inv` `div_eq_mul_inv`
`sum_apply` 📖	mathematical	—	`DFunLike.coe` `AddChar` `CommMonoid.toMonoid` `instFunLike` `Finset.sum` `instAddCommMonoid` `Finset.prod`	—	`coe_sum` `Finset.prod_apply`
`sum_eq_ite` 📖	mathematical	—	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finset.univ` `DFunLike.coe` `AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instFunLike` `instZero` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Fintype.card` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Finset.sum_congr` `Finset.sum_const` `nsmul_eq_mul` `mul_one` `ne_one_iff` `eq_zero_of_mul_eq_self_left` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `Finset.mul_sum` `Fintype.sum_equiv` `map_add_eq_mul`
`sum_eq_zero_iff_ne_zero` 📖	mathematical	—	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finset.univ` `DFunLike.coe` `AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instFunLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`sum_eq_ite` `Ne.ite_eq_right_iff` `Nat.cast_ne_zero` `Fintype.card_ne_zero` `Zero.instNonempty`
`sum_ne_zero_iff_eq_zero` 📖	mathematical	—	`AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `instZero`	—	`Iff.not_left` `sum_eq_zero_iff_ne_zero`
`toAddMonoidHomEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Additive` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Additive.addZeroClass` `Monoid.toMulOneClass` `AddMonoidHom.instFunLike` `Equiv` `AddChar` `EquivLike.toFunLike` `Equiv.instEquivLike` `toAddMonoidHomEquiv` `Additive.ofMul` `instFunLike`	—	—
`toAddMonoidHomEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddChar` `instFunLike` `Equiv` `AddMonoidHom` `Additive` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Additive.addZeroClass` `Monoid.toMulOneClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toAddMonoidHomEquiv` `Additive.toMul` `AddMonoidHom.instFunLike`	—	—
`toAddMonoidHomEquiv_symm_zero` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AddMonoidHom` `Additive` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Additive.addZeroClass` `Monoid.toMulOneClass` `AddChar` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toAddMonoidHomEquiv` `instZeroAddMonoidHom` `instZero`	—	—
`toAddMonoidHomEquiv_zero` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AddChar` `AddMonoidHom` `Additive` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Additive.addZeroClass` `Monoid.toMulOneClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `toAddMonoidHomEquiv` `instZero` `instZeroAddMonoidHom`	—	—
`toAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Additive` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Additive.addZeroClass` `Monoid.toMulOneClass` `AddMonoidHom.instFunLike` `toAddMonoidHom` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Additive.ofMul` `AddChar` `instFunLike`	—	—
`toMonoidHomEquiv_add` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AddChar` `CommMonoid.toMonoid` `MonoidHom` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Monoid.toMulOneClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `toMonoidHomEquiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoid` `MonoidHom.mul`	—	—
`toMonoidHomEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `Equiv` `AddChar` `EquivLike.toFunLike` `Equiv.instEquivLike` `toMonoidHomEquiv` `instFunLike` `Multiplicative.toAdd`	—	—
`toMonoidHomEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddChar` `instFunLike` `Equiv` `MonoidHom` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Monoid.toMulOneClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toMonoidHomEquiv` `MonoidHom.instFunLike` `Multiplicative.ofAdd`	—	—
`toMonoidHomEquiv_symm_mul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `MonoidHom` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `AddChar` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toMonoidHomEquiv` `MonoidHom.mul` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoid`	—	—
`toMonoidHomEquiv_symm_one` 📖	mathematical	—	`DFunLike.coe` `Equiv` `MonoidHom` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Monoid.toMulOneClass` `AddChar` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toMonoidHomEquiv` `instOneMonoidHom` `instZero`	—	—
`toMonoidHomEquiv_zero` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AddChar` `MonoidHom` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Monoid.toMulOneClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `toMonoidHomEquiv` `instZero` `instOneMonoidHom`	—	—
`toMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `toMonoidHom` `AddChar` `instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Multiplicative.toAdd`	—	—
`val_isUnit` 📖	mathematical	—	`IsUnit` `DFunLike.coe` `AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instFunLike`	—	`IsUnit.map` `MonoidHom.instMonoidHomClass` `Group.isUnit`
`zero_apply` 📖	mathematical	—	`DFunLike.coe` `AddChar` `instFunLike` `instZero` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—
`zpow_apply` 📖	mathematical	—	`DFunLike.coe` `AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `DivisionCommMonoid.toDivisionMonoid` `instFunLike` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroup` `DivisionCommMonoid.toCommMonoid`	—	`zsmul_apply`
`zsmul_apply` 📖	mathematical	—	`DFunLike.coe` `AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `DivisionCommMonoid.toDivisionMonoid` `instFunLike` `SubNegMonoid.toZSMul` `instAddCommGroup` `DivisionCommMonoid.toCommMonoid` `DivInvMonoid.toZPow`	—	`natCast_zsmul` `zpow_natCast` `negSucc_zsmul` `neg_apply'` `zpow_negSucc`

MonoidHom

Definitions

Name	Category	Theorems
`compAddChar` 📖	CompOp	6 math math: `compAddChar_injective_left`, `coe_compAddChar`, `AddChar.starComp_eq_inv`, `compAddChar_injective_right`, `AddChar.IsPrimitive.compMulHom_of_isPrimitive`, `compAddChar_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_compAddChar` 📖	mathematical	—	`DFunLike.coe` `AddChar` `AddChar.instFunLike` `compAddChar` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instFunLike`	—	—
`compAddChar_apply` 📖	mathematical	—	`DFunLike.coe` `AddChar` `AddChar.instFunLike` `compAddChar` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instFunLike`	—	—
`compAddChar_injective_left` 📖	mathematical	`DFunLike.coe` `AddChar` `AddChar.instFunLike`	`MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `compAddChar`	—	`DFunLike.ext'_iff` `Function.Surjective.injective_comp_right`
`compAddChar_injective_right` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instFunLike`	`AddChar` `compAddChar`	—	`DFunLike.ext'_iff` `Function.Injective.comp_left`

---

← Back to Index