Documentation Verification Report

Lemmas

📁 Source: Mathlib/Data/Int/Cast/Lemmas.lean

Statistics

Metric	Count
Definitions `castAddHom`, `castRingHom`, `ofNatHom`, `zmultiplesAddHom`, `zmultiplesHom`, `zpowersHom`, `zpowersMulHom`	7
Theorems `ext_int`, `ext_int_iff`, `apply_int`, `eq_intCastAddHom`, `ext_int`, `ext_int_iff`, `intCast_left`, `intCast_mul_intCast_mul`, `intCast_mul_left`, `intCast_mul_right`, `intCast_mul_self`, `intCast_right`, `self_intCast_mul`, `self_intCast_mul_intCast_mul`, `intCast`, `castAddHom_int`, `castRingHom_int`, `cast_comm`, `cast_commute`, `cast_dvd_cast`, `cast_eq_one`, `cast_eq_zero`, `cast_inj`, `cast_injective`, `cast_ne_one`, `cast_ne_zero`, `coe_castAddHom`, `coe_castRingHom`, `commute_cast`, `apply_mint`, `ext_int`, `ext_int_iff`, `ext_mint`, `ext_mint_iff`, `ext_int`, `ext_int_iff`, `intCast`, `subsingleton_ringHom`, `eq_intCast'`, `ext_int`, `intCast_mul_intCast_mul`, `intCast_mul_left`, `intCast_mul_right`, `eq_intCast`, `eq_intCast'`, `ext_int'`, `map_intCast`, `map_intCast'`, `zmultiplesAddHom_apply`, `zmultiplesAddHom_symm_apply`, `zmultiplesHom_apply`, `zmultiplesHom_symm_apply`, `zpowersHom_apply`, `zpowersHom_symm_apply`, `zpowersMulHom_apply`, `zpowersMulHom_symm_apply`, `zsmul_eq_mul`, `zsmul_eq_mul'`	58
Total	65

AddEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext_int` 📖	—	`DFunLike.coe` `AddEquiv` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `EquivLike.toFunLike` `instEquivLike`	—	—	`toAddMonoidHom_injective` `AddMonoidHom.ext_int`
`ext_int_iff` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `EquivLike.toFunLike` `instEquivLike`	—	`ext_int`

AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_int` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instFunLike` `SubNegMonoid.toZSMul`	—	`zmultiplesHom_symm_apply` `zmultiplesHom_apply` `Equiv.apply_symm_apply`
`eq_intCastAddHom` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `instFunLike` `AddMonoidWithOne.toOne`	`Int.castAddHom`	—	`ext_int` `Int.cast_one`
`ext_int` 📖	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `instFunLike`	—	—	`RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `ext_nat'` `instAddMonoidHomClass` `DFunLike.ext_iff` `ext` `eq_on_neg`
`ext_int_iff` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `instFunLike`	—	`ext_int`

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`intCast_left` 📖	mathematical	—	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`Int.cast_commute`
`intCast_mul_intCast_mul` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`SemiconjBy.intCast_mul_intCast_mul`
`intCast_mul_left` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	—
`intCast_mul_right` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	—
`intCast_mul_self` 📖	mathematical	—	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`intCast_mul_left` `refl`
`intCast_right` 📖	mathematical	—	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`Int.commute_cast`
`self_intCast_mul` 📖	mathematical	—	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`intCast_mul_right` `refl`
`self_intCast_mul_intCast_mul` 📖	mathematical	—	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`intCast_mul_intCast_mul` `refl`

Even

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`intCast` 📖	mathematical	`Even`	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `AddGroupWithOne.toIntCast`	—	`map` `AddMonoidHom.instAddMonoidHomClass`

Int

Definitions

Name	Category	Theorems
`castAddHom` 📖	CompOp	7 math math: `range_castAddHom`, `AddMonoidHom.eq_intCastAddHom`, `ZMod.lift_castAddHom`, `coe_castAddHom`, `ZMod.lift_comp_castAddHom`, `ZMod.ker_intCastAddHom`, `castAddHom_int`
`castRingHom` 📖	CompOp	61 math math: `NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply'`, `quotientSpanEquivZMod_comp_Quotient_mk`, `Polynomial.eval₂_intCastRingHom_X`, `CongruenceSubgroup.Gamma_mem'`, `IsPrimitiveRoot.minpoly_dvd_pow_mod`, `ModularForm.SL_slash`, `CongruenceSubgroup.conjGL_coe`, `quotientSpanNatEquivZMod_comp_Quotient_mk`, `Matrix.SpecialLinearGroup.map_intCast_injective`, `ModularGroup.sl_moeb`, `IsPrimitiveRoot.is_roots_of_minpoly`, `Matrix.SpecialLinearGroup.coe_int_neg`, `Polynomial.int_coeff_of_cyclotomic'`, `coe_castRingHom`, `Polynomial.unique_int_coeff_of_cycl`, `ModularGroup.denom_apply`, `Polynomial.int_cyclotomic_rw`, `WittVector.frobeniusPoly_zmod`, `ModularGroup.denom_S`, `Polynomial.one_le_mahlerMeasure_of_ne_zero`, `Polynomial.IsPrimitive.Int.irreducible_iff_irreducible_map_cast`, `IsPrimitiveRoot.minpoly_dvd_mod_p`, `quotientSpanEquivZMod_comp_castRingHom`, `CuspForm.coe_translate`, `IsPrimitiveRoot.separable_minpoly_mod`, `EisensteinSeries.vecMul_SL2_mem_gammaSet`, `ModularForm.SL_slash_def`, `Polynomial.IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast`, `RingOfIntegers.ZModXQuotSpanEquivQuotSpan_mk_apply`, `SlashInvariantForm.slash_action_eqn_SL''`, `IsPrimitiveRoot.squarefree_minpoly_mod`, `ZMod.ker_intCastRingHom`, `ModularGroup.im_smul_eq_div_normSq`, `Polynomial.map_cyclotomic_int`, `witt_structure_prop`, `CongruenceSubgroup.mem_conjGL`, `Matrix.SpecialLinearGroup.map_intCast_inj`, `ModularGroup.tendsto_lcRow0`, `SL_reduction_mod_hom_val`, `Padic.comap_mulValuation_eq_int_padicValuation`, `CongruenceSubgroup.mem_conjGL'`, `WittVector.map_frobeniusPoly`, `ModularGroup.exists_one_half_le_im_smul_and_norm_denom_le`, `ModularForm.is_invariant_one'`, `RingHom.eq_intCast'`, `algebraMap_int_eq`, `IsPrimitiveRoot.pow_isRoot_minpoly`, `Matrix.SpecialLinearGroup.coe_matrix_coe`, `ModularForm.SL_slash_apply`, `EisensteinSeries.eisSummand_SL2_apply`, `Polynomial.ringHom_eval₂_intCastRingHom`, `MonoidWithZeroHomClass.ext_rat_iff`, `MvPolynomial.C_dvd_iff_zmod`, `map_wittStructureInt`, `Polynomial.finite_mahlerMeasure_le`, `EisensteinSeries.eisensteinSeries_slash_apply`, `quotientSpanNatEquivZMod_comp_castRingHom`, `Polynomial.card_mahlerMeasure_le_prod`, `ModularGroup.smul_eq_lcRow0_add`, `castRingHom_int`, `Polynomial.int_cyclotomic_spec`
`ofNatHom` 📖	CompOp	2 math math: `MonoidWithZeroHom.ext_int_iff`, `MonoidHom.ext_int_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`castAddHom_int` 📖	mathematical	—	`castAddHom` `Ring.toAddGroupWithOne` `instRing` `AddMonoidHom.id` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddMonoid`	—	`AddMonoidHom.eq_intCastAddHom`
`castRingHom_int` 📖	mathematical	—	`castRingHom` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `instCommRing` `RingHom.id` `Semiring.toNonAssocSemiring` `instSemiring`	—	`RingHom.eq_intCast'`
`cast_comm` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`Commute.eq` `cast_commute`
`cast_commute` 📖	mathematical	—	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`cast_natCast` `Nat.cast_commute` `cast_negSucc`
`cast_dvd_cast` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`map_dvd` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass`
`cast_eq_one` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`cast_one`
`cast_eq_zero` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddGroupWithOne.toAddGroup`	—	`Nat.cast_eq_zero` `cast_natCast` `neg_eq_zero` `cast_negSucc` `cast_zero`
`cast_inj` 📖	mathematical	—	`AddGroupWithOne.toIntCast`	—	`sub_eq_zero` `cast_sub` `cast_eq_zero`
`cast_injective` 📖	mathematical	—	`AddGroupWithOne.toIntCast`	—	—
`cast_ne_one` 📖	—	—	—	—	`Iff.not` `cast_eq_one`
`cast_ne_zero` 📖	—	—	—	—	`cast_eq_zero`
`coe_castAddHom` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddMonoid` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `AddMonoidHom.instFunLike` `castAddHom` `AddGroupWithOne.toIntCast`	—	—
`coe_castRingHom` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `instSemiring` `NonAssocRing.toNonAssocSemiring` `RingHom.instFunLike` `castRingHom` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	—
`commute_cast` 📖	mathematical	—	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`Commute.symm` `cast_commute`

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_mint` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instFunLike` `DivInvMonoid.toZPow` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Multiplicative.ofAdd` `Multiplicative.toAdd`	—	`zpowersHom_symm_apply` `zpowersHom_apply` `Equiv.apply_symm_apply`
`ext_int` 📖	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Int.instSemiring` `Monoid.toMulOneClass` `instFunLike` `comp` `Nat.instNonAssocSemiring` `RingHom.toMonoidHom` `Int.ofNatHom`	—	—	`ext` `DFunLike.congr_fun` `neg_one_mul` `map_mul` `Nat.cast_one`
`ext_int_iff` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Int.instSemiring` `Monoid.toMulOneClass` `instFunLike` `comp` `Nat.instNonAssocSemiring` `RingHom.toMonoidHom` `Int.ofNatHom`	—	`ext_int`
`ext_mint` 📖	—	`DFunLike.coe` `MonoidHom` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `Monoid.toMulOneClass` `instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Multiplicative.ofAdd`	—	—	`Equiv.injective` `AddMonoidHom.ext_int`
`ext_mint_iff` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `Monoid.toMulOneClass` `instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Multiplicative.ofAdd`	—	`ext_mint`

MonoidWithZeroHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext_int` 📖	—	`DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Int.instSemiring` `MonoidWithZero.toMulZeroOneClass` `funLike` `comp` `Nat.instNonAssocSemiring` `RingHom.toMonoidWithZeroHom` `Int.ofNatHom`	—	—	`toMonoidHom_injective` `MonoidHom.ext_int` `MonoidHom.ext` `DFunLike.congr_fun`
`ext_int_iff` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Int.instSemiring` `MonoidWithZero.toMulZeroOneClass` `funLike` `comp` `Nat.instNonAssocSemiring` `RingHom.toMonoidWithZeroHom` `Int.ofNatHom`	—	`ext_int`

Odd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`intCast` 📖	mathematical	`Odd` `Int.instSemiring`	`Ring.toSemiring` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`map` `RingHom.instRingHomClass`

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_intCast'` 📖	mathematical	—	`Int.castRingHom`	—	`ext` `eq_intCast` `instRingHomClass`
`ext_int` 📖	—	—	—	—	`coe_addMonoidHom_injective` `AddMonoidHom.ext_int` `RingHomClass.toAddMonoidHomClass` `instRingHomClass` `map_one`

RingHom.Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`subsingleton_ringHom` 📖	mathematical	—	`RingHom` `Semiring.toNonAssocSemiring` `Int.instSemiring`	—	`RingHom.ext_int`

SemiconjBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`intCast_mul_intCast_mul` 📖	mathematical	`SemiconjBy` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	—
`intCast_mul_left` 📖	mathematical	`SemiconjBy` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`mul_left` `Int.cast_commute`
`intCast_mul_right` 📖	mathematical	`SemiconjBy` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`mul_right` `Int.commute_cast`

(root)

Definitions

Name	Category	Theorems
`zmultiplesAddHom` 📖	CompOp	2 math math: `zmultiplesAddHom_symm_apply`, `zmultiplesAddHom_apply`
`zmultiplesHom` 📖	CompOp	5 math math: `AddSubgroup.range_zmultiplesHom`, `zmultiplesHom_ker_eq`, `Int.tendsto_zmultiplesHom_cofinite`, `zmultiplesHom_apply`, `zmultiplesHom_symm_apply`
`zpowersHom` 📖	CompOp	4 math math: `zpowersHom_symm_apply`, `zpowersHom_apply`, `Subgroup.range_zpowersHom`, `zpowersHom_ker_eq`
`zpowersMulHom` 📖	CompOp	2 math math: `zpowersMulHom_symm_apply`, `zpowersMulHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_intCast` 📖	mathematical	—	`DFunLike.coe` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`eq_intCast'` `RingHomClass.toAddMonoidHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass`
`eq_intCast'` 📖	mathematical	`DFunLike.coe` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	`AddGroupWithOne.toIntCast`	—	`DFunLike.ext_iff` `AddMonoidHom.eq_intCastAddHom`
`ext_int'` 📖	—	`DFunLike.coe`	—	—	`DFunLike.ext` `DFunLike.congr_fun` `MonoidWithZeroHom.ext_int` `MonoidWithZeroHom.ext_nat`
`map_intCast` 📖	mathematical	—	`DFunLike.coe` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`eq_intCast` `RingHom.instRingHomClass`
`map_intCast'` 📖	mathematical	`DFunLike.coe` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	`AddGroupWithOne.toIntCast`	—	`eq_intCast'` `AddMonoidHom.instAddMonoidHomClass` `Int.cast_one`
`zmultiplesAddHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoidHom.instFunLike` `AddEquiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `AddMonoidHom.add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `zmultiplesAddHom` `SubNegMonoid.toZSMul`	—	—
`zmultiplesAddHom_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoidHom.add` `AddCommGroup.toAddCommMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `zmultiplesAddHom` `AddMonoidHom.instFunLike`	—	—
`zmultiplesHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `zmultiplesHom` `SubNegMonoid.toZSMul`	—	—
`zmultiplesHom_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `zmultiplesHom` `AddMonoidHom.instFunLike`	—	—
`zpowersHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `zpowersHom` `DivInvMonoid.toZPow` `Multiplicative.toAdd`	—	—
`zpowersHom_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `MonoidHom` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `zpowersHom` `MonoidHom.instFunLike` `Multiplicative.ofAdd`	—	—
`zpowersMulHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `MonoidHom.instFunLike` `MulEquiv` `MulOne.toMul` `MonoidHom.mul` `CommGroup.toCommMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `zpowersMulHom` `DivInvMonoid.toZPow` `Equiv` `Equiv.instEquivLike` `Multiplicative.toAdd`	—	—
`zpowersMulHom_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MonoidHom` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `MonoidHom.mul` `CommGroup.toCommMonoid` `MulOne.toMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `zpowersMulHom` `MonoidHom.instFunLike` `Equiv` `Equiv.instEquivLike` `Multiplicative.ofAdd`	—	—
`zsmul_eq_mul` 📖	mathematical	—	`SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `AddGroupWithOne.toIntCast`	—	`natCast_zsmul` `nsmul_eq_mul` `Int.cast_natCast` `negSucc_zsmul` `Nat.cast_succ` `add_mul` `Distrib.rightDistribClass` `one_mul` `neg_add_rev` `Int.cast_negSucc` `neg_mul`
`zsmul_eq_mul'` 📖	mathematical	—	`SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `AddGroupWithOne.toIntCast`	—	`zsmul_eq_mul` `Commute.eq` `Int.cast_commute`

---

← Back to Index