ForwardDiff

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

Statistics

Metric	Count
Definitions `fwdDiff`, `«termΔ_[_]»`, `fwdDiffₗ`, `shiftₗ`	4
Theorems `fwdDiff_iter_degree_add_one_eq_zero`, `fwdDiff_iter_degree_eq_factorial`, `fwdDiff_iter_eq_zero_of_degree_lt`, `fwdDiff_add`, `fwdDiff_addChar_eq`, `coe_fwdDiffₗ`, `coe_fwdDiffₗ_pow`, `fwdDiffₗ_apply`, `shiftₗ_apply`, `shiftₗ_pow_apply`, `fwdDiff_choose`, `fwdDiff_comp_add`, `fwdDiff_const`, `fwdDiff_const_smul`, `fwdDiff_finset_sum`, `fwdDiff_iter_add`, `fwdDiff_iter_choose`, `fwdDiff_iter_choose_zero`, `fwdDiff_iter_comp_add`, `fwdDiff_iter_const_smul`, `fwdDiff_iter_eq_factorial`, `fwdDiff_iter_eq_sum_shift`, `fwdDiff_iter_finset_sum`, `fwdDiff_iter_pow_eq_zero_of_lt`, `fwdDiff_iter_sum_mul_pow_eq_zero`, `fwdDiff_smul`, `fwdDiff_smul_const`, `shift_eq_sum_fwdDiff_iter`	28
Total	32

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fwdDiff_iter_degree_add_one_eq_zero` 📖	mathematical	—	`Nat.iterate` `fwdDiff` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `eval` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`fwdDiff_iter_eq_zero_of_degree_lt`
`fwdDiff_iter_degree_eq_factorial` 📖	mathematical	—	`Nat.iterate` `fwdDiff` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `eval` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `DistribSMul.toSMulZeroClass` `instDistribSMul` `leadingCoeff` `Pi.instNatCast` `AddMonoidWithOne.toNatCast` `Nat.factorial`	—	`eval_eq_sum_range` `Finset.sum_apply` `fwdDiff_iter_finset_sum` `Finset.sum_congr` `fwdDiff_iter_const_smul` `Finset.sum_range_succ` `Finset.sum_eq_zero` `fwdDiff_iter_pow_eq_zero_of_lt` `Finset.mem_range` `smul_zero` `Pi.zero_apply` `zero_add` `fwdDiff_iter_eq_factorial` `leadingCoeff.eq_1` `Pi.smul_apply`
`fwdDiff_iter_eq_zero_of_degree_lt` 📖	mathematical	`natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Nat.iterate` `fwdDiff` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `eval` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`add_assoc` `add_comm` `Function.iterate_add_apply` `Function.iterate_succ_apply` `fwdDiff_iter_degree_eq_factorial` `Pi.smul_def` `fwdDiff_const` `fwdDiff_iter_eq_sum_shift` `Finset.sum_congr` `smul_zero` `Finset.sum_const_zero`

(root)

Definitions

Name	Category	Theorems
`fwdDiff` 📖	CompOp	32 math math: `fwdDiff_const`, `fwdDiff_iter_pow_eq_zero_of_lt`, `fwdDiff_finset_sum`, `fwdDiff_iter_comp_add`, `fwdDiff_iter_finset_sum`, `fwdDiff_const_smul`, `PadicInt.fwdDiff_tendsto_zero`, `fwdDiff_iter_eq_sum_shift`, `Polynomial.fwdDiff_iter_degree_add_one_eq_zero`, `IsUltrametricDist.norm_fwdDiff_iter_apply_le`, `Polynomial.fwdDiff_iter_eq_zero_of_degree_lt`, `fwdDiff_choose`, `fwdDiff_iter_choose_zero`, `fwdDiff_iter_add`, `fwdDiff_aux.fwdDiffₗ_apply`, `PadicInt.fwdDiff_iter_le_of_forall_le`, `fwdDiff_smul`, `fwdDiff_iter_eq_factorial`, `PadicInt.hasSum_mahler`, `PadicInt.fwdDiff_mahlerSeries`, `PadicInt.mahlerEquiv_apply`, `Polynomial.fwdDiff_iter_degree_eq_factorial`, `fwdDiff_addChar_eq`, `fwdDiff_comp_add`, `fwdDiff_add`, `fwdDiff_aux.coe_fwdDiffₗ_pow`, `fwdDiff_smul_const`, `fwdDiff_iter_sum_mul_pow_eq_zero`, `shift_eq_sum_fwdDiff_iter`, `fwdDiff_aux.coe_fwdDiffₗ`, `fwdDiff_iter_const_smul`, `fwdDiff_iter_choose`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fwdDiff_add` 📖	mathematical	—	`fwdDiff` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`add_sub_add_comm`
`fwdDiff_addChar_eq` 📖	mathematical	—	`Nat.iterate` `fwdDiff` `Ring.toAddCommGroup` `DFunLike.coe` `AddChar` `AddCommMonoid.toAddMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `AddChar.instFunLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`pow_zero` `one_mul` `Function.iterate_succ_apply'` `pow_succ` `mul_assoc` `sub_mul` `AddChar.map_add_eq_mul` `add_comm`
`fwdDiff_choose` 📖	mathematical	—	`fwdDiff` `Nat.instAddCommMonoid` `Int.instAddCommGroup` `Nat.choose`	—	`Nat.cast_add` `add_sub_cancel_right`
`fwdDiff_comp_add` 📖	mathematical	—	`fwdDiff` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`fwdDiff_iter_comp_add`
`fwdDiff_const` 📖	mathematical	—	`fwdDiff` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`sub_self`
`fwdDiff_const_smul` 📖	mathematical	—	`fwdDiff` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	`smul_sub`
`fwdDiff_finset_sum` 📖	mathematical	—	`fwdDiff` `Finset.sum` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid`	—	`map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`fwdDiff_iter_add` 📖	mathematical	—	`Nat.iterate` `fwdDiff` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`fwdDiff_aux.coe_fwdDiffₗ_pow` `map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass`
`fwdDiff_iter_choose` 📖	mathematical	—	`Nat.iterate` `fwdDiff` `Nat.instAddCommMonoid` `Int.instAddCommGroup` `Nat.choose`	—	`zero_add` `add_assoc` `add_comm` `Function.iterate_succ_apply'` `fwdDiff_choose`
`fwdDiff_iter_choose_zero` 📖	mathematical	—	`Nat.iterate` `fwdDiff` `Nat.instAddCommMonoid` `Int.instAddCommGroup` `Nat.choose`	—	`lt_trichotomy` `LT.lt.ne'` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Function.iterate_add_apply` `fwdDiff_iter_choose` `add_zero` `Nat.choose_zero_right` `Function.iterate_one` `Nat.cast_one` `fwdDiff_const` `fwdDiff_iter_eq_sum_shift` `Finset.sum_congr` `smul_zero` `Finset.sum_const_zero` `LT.lt.ne` `add_assoc` `Nat.cast_zero`
`fwdDiff_iter_comp_add` 📖	mathematical	—	`Nat.iterate` `fwdDiff` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`fwdDiff_iter_eq_sum_shift` `Finset.sum_congr` `add_right_comm`
`fwdDiff_iter_const_smul` 📖	mathematical	—	`Nat.iterate` `fwdDiff` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	`fwdDiff_const_smul`
`fwdDiff_iter_eq_factorial` 📖	mathematical	—	`Nat.iterate` `fwdDiff` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Pi.instNatCast` `AddMonoidWithOne.toNatCast` `Nat.factorial`	—	`pow_zero` `Nat.cast_one` `add_pow` `Finset.sum_congr` `one_pow` `mul_one` `Finset.sum_range_succ` `Nat.choose_succ_self_right` `Nat.cast_add` `Nat.choose_self` `mul_comm` `one_mul` `add_sub_cancel_right` `nsmul_eq_mul` `Finset.sum_apply` `fwdDiff_iter_finset_sum` `fwdDiff_iter_const_smul` `Nat.cast_mul` `Pi.instIsRightCancelAdd` `AddRightCancelSemigroup.toIsRightCancelAdd` `Finset.sum_eq_zero` `fwdDiff_iter_pow_eq_zero_of_lt` `Finset.mem_range` `MulZeroClass.mul_zero`
`fwdDiff_iter_eq_sum_shift` 📖	mathematical	—	`Nat.iterate` `fwdDiff` `Finset.sum` `AddCommGroup.toAddCommMonoid` `Finset.range` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Monoid.toNatPow` `Int.instMonoid` `Nat.choose` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid`	—	`add_sub_cancel_right` `fwdDiff_aux.coe_fwdDiffₗ` `Module.End.pow_apply` `Commute.neg_right` `Commute.one_right` `sub_eq_add_neg` `LinearMap.sum_apply` `Finset.sum_apply` `Nat.cast_one` `Int.cast_natCast` `Int.cast_mul` `Int.cast_pow` `Int.cast_neg` `Int.cast_one` `mul_assoc` `Module.End.mul_apply` `Module.End.intCast_apply` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Pi.smul_apply` `fwdDiff_aux.shiftₗ_pow_apply` `LinearMap.congr_fun` `Commute.add_pow`
`fwdDiff_iter_finset_sum` 📖	mathematical	—	`Nat.iterate` `fwdDiff` `Finset.sum` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid`	—	`fwdDiff_aux.coe_fwdDiffₗ_pow` `Finset.sum_congr` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`fwdDiff_iter_pow_eq_zero_of_lt` 📖	mathematical	—	`Nat.iterate` `fwdDiff` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Nat.instCanonicallyOrderedAdd` `add_pow` `Finset.sum_congr` `one_pow` `mul_one` `Finset.sum_range_succ` `Nat.choose_self` `Nat.cast_one` `add_sub_cancel_right` `nsmul_eq_mul` `mul_comm` `Finset.sum_apply` `Function.iterate_succ_apply` `fwdDiff_iter_finset_sum` `Finset.sum_eq_zero` `fwdDiff_iter_const_smul` `Finset.mem_range` `nsmul_zero`
`fwdDiff_iter_sum_mul_pow_eq_zero` 📖	mathematical	—	`Nat.iterate` `fwdDiff` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Finset.sum` `Finset.range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Finset.sum_apply` `fwdDiff_iter_finset_sum` `Finset.sum_fn` `Finset.sum_congr` `fwdDiff_iter_const_smul` `Finset.sum_eq_zero` `smul_eq_zero_of_right` `fwdDiff_iter_pow_eq_zero_of_lt` `Finset.mem_range`
`fwdDiff_smul` 📖	mathematical	—	`fwdDiff` `Pi.smul'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Ring.toAddCommGroup`	—	`sub_smul` `smul_sub` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.const_add_termg` `add_zero` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsInt.neg_to_eq` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Abel.zero_termg`
`fwdDiff_smul_const` 📖	mathematical	—	`fwdDiff` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Pi.smul'` `Ring.toAddCommGroup`	—	`sub_smul`
`shift_eq_sum_fwdDiff_iter` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `Finset.sum` `AddCommGroup.toAddCommMonoid` `Finset.range` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Nat.choose` `Nat.iterate` `fwdDiff`	—	`fwdDiff_aux.shiftₗ_pow_apply` `fwdDiff_aux.shiftₗ.eq_1` `Finset.sum_congr` `one_pow` `mul_one` `LinearMap.coe_sum` `Finset.sum_apply` `LinearMap.map_smul_of_tower` `LinearMap.IsScalarTower.compatibleSMul` `AddCommMonoid.nat_isScalarTower` `Module.End.pow_apply` `LinearMap.congr_fun` `Commute.add_pow` `Commute.one_right`

fwdDiff

Definitions

Name	Category	Theorems
`«termΔ_[_]»` 📖	CompOp	—

fwdDiff_aux

Definitions

Name	Category	Theorems
`fwdDiffₗ` 📖	CompOp	3 math math: `fwdDiffₗ_apply`, `coe_fwdDiffₗ_pow`, `coe_fwdDiffₗ`
`shiftₗ` 📖	CompOp	2 math math: `shiftₗ_pow_apply`, `shiftₗ_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_fwdDiffₗ` 📖	mathematical	—	`DFunLike.coe` `Module.End` `Int.instSemiring` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `AddCommGroup.toIntModule` `Pi.addCommGroup` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring` `fwdDiffₗ` `fwdDiff`	—	—
`coe_fwdDiffₗ_pow` 📖	mathematical	—	`DFunLike.coe` `Module.End` `Int.instSemiring` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `AddCommGroup.toIntModule` `Pi.addCommGroup` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `Module.End.instMonoid` `fwdDiffₗ` `Nat.iterate` `fwdDiff`	—	`Module.End.pow_apply` `coe_fwdDiffₗ`
`fwdDiffₗ_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Int.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `AddCommGroup.toIntModule` `Pi.addCommGroup` `LinearMap.instFunLike` `fwdDiffₗ` `fwdDiff`	—	—
`shiftₗ_apply` 📖	mathematical	—	`DFunLike.coe` `Module.End` `Int.instSemiring` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `AddCommGroup.toIntModule` `Pi.addCommGroup` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring` `shiftₗ` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`sub_add_cancel`
`shiftₗ_pow_apply` 📖	mathematical	—	`DFunLike.coe` `Module.End` `Int.instSemiring` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `AddCommGroup.toIntModule` `Pi.addCommGroup` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `Module.End.instMonoid` `shiftₗ` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid`	—	`pow_zero` `zero_nsmul` `add_zero` `pow_add` `pow_one` `shiftₗ_apply` `add_assoc` `add_nsmul` `one_smul`

---

← Back to Index