GeomSum

📁 Source: Mathlib/Algebra/Ring/GeomSum.lean

Statistics

Metric	Count
Definitions	0
Theorems `geom_sum₂_Ico_mul`, `geom_sum₂_comm`, `geom_sum₂_mul`, `geom_sum₂_mul_add`, `geom_sum₂_succ_eq`, `mul_geom_sum₂`, `mul_geom_sum₂_Ico`, `mul_neg_geom_sum₂`, `sub_dvd_pow_sub_pow`, `pow_sub_one_mul_geom_sum_eq_pow_sub_one_mul_geom_sum`, `geomSum_eq`, `nat_pow_one_sub_dvd_pow_mul_sub_one`, `nat_sub_dvd_pow_sub_pow`, `pow_sub_one_dvd_pow_sub_one`, `pow_sub_pow_dvd_pow_sub_pow`, `sub_dvd_pow_sub_pow`, `sub_one_dvd_pow_sub_one`, `add_dvd_pow_add_pow`, `nat_add_dvd_pow_add_pow`, `map_geom_sum`, `map_geom_sum₂`, `dvd_pow_pow_sub_self_of_dvd`, `dvd_pow_sub_one_of_dvd`, `geom_sum_Ico_mul`, `geom_sum_Ico_mul_neg`, `geom_sum_mul`, `geom_sum_mul_add`, `geom_sum_mul_neg`, `geom_sum_mul_of_le_one`, `geom_sum_mul_of_one_le`, `geom_sum_one`, `geom_sum_succ`, `geom_sum_succ'`, `geom_sum_two`, `geom_sum_zero`, `geom_sum₂_comm`, `geom_sum₂_mul`, `geom_sum₂_mul_add`, `geom_sum₂_mul_of_ge`, `geom_sum₂_mul_of_le`, `geom_sum₂_self`, `geom_sum₂_succ_eq`, `geom_sum₂_with_one`, `mul_geom_sum`, `mul_geom_sum₂_Ico`, `mul_neg_geom_sum`, `neg_one_geom_sum`, `one_geom_sum`, `one_sub_dvd_one_sub_pow`, `op_geom_sum`, `op_geom_sum₂`, `pow_one_sub_dvd_pow_mul_sub_one`, `pow_sub_one_mul_geom_sum_eq_pow_sub_one_mul_geom_sum`, `sub_dvd_pow_sub_pow`, `sub_one_dvd_pow_sub_one`, `zero_geom_sum`	56
Total	56

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`geom_sum₂_Ico_mul` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`MulOpposite.op_injective` `Finset.op_sum` `Finset.sum_congr` `pow_pow` `op` `symm` `mul_geom_sum₂_Ico`
`geom_sum₂_comm` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`Finset.sum_congr` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `pow_zero` `mul_one` `Finset.sum_flip` `Finset.mem_range` `pow_pow`
`geom_sum₂_mul` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`geom_sum₂_mul_add` `sub_left` `refl` `sub_add_cancel` `add_sub_cancel_right`
`geom_sum₂_mul_add` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Distrib.toAdd` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`Finset.range_zero` `Finset.sum_empty` `MulZeroClass.zero_mul` `zero_add` `pow_zero` `tsub_add_eq_tsub_tsub` `Nat.instOrderedSub` `tsub_self` `Nat.instCanonicallyOrderedAdd` `mul_one` `pow_right` `add_right` `symm` `refl` `mul_assoc` `eq` `pow_succ'` `add_tsub_cancel_right` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `add_comm` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Finset.mem_range` `add_assoc` `add_mul` `Distrib.rightDistribClass` `Finset.sum_range_succ_comm` `Finset.sum_congr` `Finset.mul_sum` `mul_add` `Distrib.leftDistribClass`
`geom_sum₂_succ_eq` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Distrib.toAdd`	—	`Finset.mul_sum` `Finset.sum_range_succ_comm` `tsub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `pow_zero` `mul_one` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Finset.sum_congr` `eq` `pow_right` `symm` `mul_assoc` `Finset.mem_range`
`mul_geom_sum₂` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	—	`neg_sub` `mul_neg_geom_sum₂` `neg_mul`
`mul_geom_sum₂_Ico` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	—	`Finset.sum_Ico_eq_sub` `Finset.sum_congr` `pow_add` `Finset.mem_range` `pow_mul_comm` `Finset.sum_mul` `mul_sub` `mul_geom_sum₂` `mul_assoc` `sub_mul` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `sub_sub_sub_cancel_right`
`mul_neg_geom_sum₂` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	—	`MulOpposite.op_injective` `Finset.op_sum` `Finset.sum_congr` `op_geom_sum₂` `geom_sum₂_mul` `op` `symm`
`sub_dvd_pow_sub_pow` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`Dvd.intro` `mul_geom_sum₂`

IsPrimitiveRoot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pow_sub_one_mul_geom_sum_eq_pow_sub_one_mul_geom_sum` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.range`	—	`pow_sub_one_mul_geom_sum_eq_pow_sub_one_mul_geom_sum`

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`geomSum_eq` 📖	mathematical	—	`Finset.sum` `instAddCommMonoid` `Finset.range` `Monoid.toNatPow` `instMonoid`	—	`tsub_pos_iff_lt` `instCanonicallyOrderedAdd` `instOrderedSub` `tsub_eq_of_eq_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `Finset.sum_congr` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `geom_sum_mul_add`
`nat_pow_one_sub_dvd_pow_mul_sub_one` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid`	—	`sub_one_dvd_pow_sub_one`
`nat_sub_dvd_pow_sub_pow` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid`	—	`sub_dvd_pow_sub_pow`
`pow_sub_one_dvd_pow_sub_one` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid`	—	`one_pow` `pow_sub_pow_dvd_pow_sub_pow`
`pow_sub_pow_dvd_pow_sub_pow` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid`	—	`pow_mul` `sub_dvd_pow_sub_pow`
`sub_dvd_pow_sub_pow` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid`	—	`le_or_gt` `sub_dvd_pow_sub_pow` `LT.lt.le` `dvd_zero`
`sub_one_dvd_pow_sub_one` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid`	—	`one_pow` `sub_dvd_pow_sub_pow`

Odd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_dvd_pow_add_pow` 📖	mathematical	`Odd` `Nat.instSemiring`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`geom_sum₂_mul` `Dvd.intro_left` `sub_neg_eq_add` `neg_pow`
`nat_add_dvd_pow_add_pow` 📖	mathematical	`Odd` `Nat.instSemiring`	`Monoid.toNatPow` `Nat.instMonoid`	—	`add_dvd_pow_add_pow`

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_geom_sum` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `instFunLike` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`map_sum` `RingHomClass.toAddMonoidHomClass` `instRingHomClass` `Finset.sum_congr` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass`
`map_geom_sum₂` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `instFunLike` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finset.range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`map_sum` `RingHomClass.toAddMonoidHomClass` `instRingHomClass` `Finset.sum_congr` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_pow_pow_sub_self_of_dvd` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid`	—	`pow_zero` `pow_one` `sub_self` `dvd_zero` `zero_dvd_iff` `zero_pow` `dvd_refl` `pos_of_ne_zero` `Nat.instCanonicallyOrderedAdd` `pow_succ'` `mul_sub_one` `mul_dvd_mul_left` `dvd_pow_sub_one_of_dvd` `Nat.cast_sub` `Nat.cast_pow`
`dvd_pow_sub_one_of_dvd` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`pow_one_sub_dvd_pow_mul_sub_one`
`geom_sum_Ico_mul` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`Finset.sum_Ico_eq_sub` `sub_mul` `geom_sum_mul` `sub_sub_sub_cancel_right`
`geom_sum_Ico_mul_neg` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`Finset.sum_Ico_eq_sub` `sub_mul` `geom_sum_mul_neg` `sub_sub_sub_cancel_left`
`geom_sum_mul` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`Commute.geom_sum₂_mul` `Commute.one_right` `geom_sum₂_with_one` `one_pow`
`geom_sum_mul_add` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Commute.geom_sum₂_mul_add` `Commute.one_right` `geom_sum₂_with_one` `one_pow`
`geom_sum_mul_neg` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`geom_sum_mul` `neg_sub` `mul_neg`
`geom_sum_mul_of_le_one` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`Finset.sum_congr` `one_pow` `mul_one` `geom_sum₂_mul_of_le`
`geom_sum_mul_of_one_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`Finset.sum_congr` `one_pow` `mul_one` `geom_sum₂_mul_of_ge`
`geom_sum_one` 📖	mathematical	—	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Finset.sum_singleton` `pow_zero`
`geom_sum_succ` 📖	mathematical	—	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Finset.sum_range_succ'` `pow_zero` `Finset.mul_sum` `Finset.sum_congr`
`geom_sum_succ'` 📖	mathematical	—	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	`Finset.sum_range_succ` `add_comm`
`geom_sum_two` 📖	mathematical	—	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`geom_sum_succ'` `pow_one` `Finset.sum_singleton` `pow_zero`
`geom_sum_zero` 📖	mathematical	—	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`geom_sum₂_comm` 📖	mathematical	—	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finset.range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`Commute.geom_sum₂_comm` `Commute.all`
`geom_sum₂_mul` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Commute.geom_sum₂_mul` `Commute.all`
`geom_sum₂_mul_add` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Distrib.toMul` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`Commute.geom_sum₂_mul_add` `Commute.all`
`geom_sum₂_mul_of_ge` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`eq_tsub_of_add_eq` `Finset.sum_congr` `tsub_add_cancel_of_le` `geom_sum₂_mul_add`
`geom_sum₂_mul_of_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`Finset.sum_range_reflect` `Finset.sum_congr` `mul_comm` `geom_sum₂_mul_of_ge`
`geom_sum₂_self` 📖	mathematical	—	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Finset.sum_congr` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `Finset.mem_range` `Finset.sum_const` `Finset.card_range` `nsmul_eq_mul`
`geom_sum₂_succ_eq` 📖	mathematical	—	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Distrib.toAdd`	—	`Commute.geom_sum₂_succ_eq` `Commute.all`
`geom_sum₂_with_one` 📖	mathematical	—	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Finset.sum_congr` `one_pow` `mul_one`
`mul_geom_sum` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	—	`MulOpposite.op_injective` `Finset.op_sum` `Finset.sum_congr` `geom_sum_mul`
`mul_geom_sum₂_Ico` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`Commute.mul_geom_sum₂_Ico` `Commute.all`
`mul_neg_geom_sum` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	—	`MulOpposite.op_injective` `Finset.op_sum` `Finset.sum_congr` `geom_sum_mul_neg`
`neg_one_geom_sum` 📖	mathematical	—	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Even` `Nat.instDecidablePredEven` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`geom_sum_succ'` `Even.neg_one_pow` `add_zero` `Odd.neg_one_pow` `Nat.not_even_iff_odd` `neg_add_cancel`
`one_geom_sum` 📖	mathematical	—	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddMonoidWithOne.toNatCast`	—	`Finset.sum_congr` `one_pow` `Finset.sum_const` `Finset.card_range` `nsmul_eq_mul` `mul_one`
`one_sub_dvd_one_sub_pow` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`one_pow` `Commute.sub_dvd_pow_sub_pow` `Commute.one_left`
`op_geom_sum` 📖	mathematical	—	`MulOpposite.op` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulOpposite` `MulOpposite.instAddCommMonoid` `MulOpposite.instMonoid`	—	`Finset.op_sum` `Finset.sum_congr`
`op_geom_sum₂` 📖	mathematical	—	`Finset.sum` `MulOpposite` `MulOpposite.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.range` `MulOpposite.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Monoid.toNatPow` `MulOpposite.instMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulOpposite.op`	—	`Finset.sum_range_reflect` `Finset.sum_congr`
`pow_one_sub_dvd_pow_mul_sub_one` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`pow_mul` `sub_one_dvd_pow_sub_one`
`pow_sub_one_mul_geom_sum_eq_pow_sub_one_mul_geom_sum` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.range`	—	—
`sub_dvd_pow_sub_pow` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`Commute.sub_dvd_pow_sub_pow` `Commute.all`
`sub_one_dvd_pow_sub_one` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`one_pow` `Commute.sub_dvd_pow_sub_pow` `Commute.one_right`
`zero_geom_sum` 📖	mathematical	—	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Finset.sum_singleton` `pow_zero` `geom_sum_succ'` `zero_pow` `zero_add` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat`

---

← Back to Index