Intervals

📁 Source: Mathlib/Algebra/BigOperators/Intervals.lean

Statistics

Metric	Count
Definitions	0
Theorems `prod_Icc_div`, `prod_Iic_div`, `sum_Icc_sub`, `sum_Iic_sub`, `prod_Icc_div`, `prod_Icc_succ_top`, `prod_Ico_add`, `prod_Ico_add'`, `prod_Ico_add_right_sub_eq`, `prod_Ico_consecutive`, `prod_Ico_div`, `prod_Ico_div_bot`, `prod_Ico_eq_div`, `prod_Ico_eq_mul_inv`, `prod_Ico_eq_prod_range`, `prod_Ico_id_eq_factorial`, `prod_Ico_reflect`, `prod_Ico_succ_div_top`, `prod_Ico_succ_top`, `prod_Ioc_consecutive`, `prod_Ioc_succ_top`, `prod_fin_Icc_eq_prod_nat_Icc`, `prod_range_diag_flip`, `prod_range_div_prod_range`, `prod_range_eq_mul_Ico`, `prod_range_mul_prod_Ico`, `prod_range_reflect`, `prod_range_succ_div_prod`, `prod_range_succ_div_top`, `sum_Icc_sub`, `sum_Icc_succ_top`, `sum_Ico_Ico_comm`, `sum_Ico_Ico_comm'`, `sum_Ico_add`, `sum_Ico_add'`, `sum_Ico_add_right_sub_eq`, `sum_Ico_consecutive`, `sum_Ico_eq_add_neg`, `sum_Ico_eq_sub`, `sum_Ico_eq_sum_range`, `sum_Ico_reflect`, `sum_Ico_sub`, `sum_Ico_sub_bot`, `sum_Ico_succ_sub_top`, `sum_Ico_succ_top`, `sum_Ioc_consecutive`, `sum_Ioc_succ_top`, `sum_fin_Icc_eq_sum_nat_Icc`, `sum_range_add_sum_Ico`, `sum_range_diag_flip`, `sum_range_eq_add_Ico`, `sum_range_id`, `sum_range_id_mul_two`, `sum_range_reflect`, `sum_range_sub_sum_range`, `sum_range_succ_sub_sum`, `sum_range_succ_sub_top`	57
Total	57

Fin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_Icc_div` 📖	mathematical	—	`Finset.prod` `CommGroup.toCommMonoid` `Finset.Icc` `PartialOrder.toPreorder` `instPartialOrder` `instLocallyFiniteOrder` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	`Finset.prod_fin_Icc_eq_prod_nat_Icc` `Finset.prod_congr` `Nat.instNoMaxOrder` `Finset.prod_Icc_div`
`prod_Iic_div` 📖	mathematical	—	`Finset.prod` `CommGroup.toCommMonoid` `Finset.Iic` `PartialOrder.toPreorder` `instPartialOrder` `instLocallyFiniteOrderBot` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	`Finset.prod_ite_mem_eq` `Finset.prod_fin_eq_prod_range` `Finset.prod_congr_of_eq_on_inter` `Nat.instNoMaxOrder` `Finset.prod_range_div`
`sum_Icc_sub` 📖	mathematical	—	`Finset.sum` `AddCommGroup.toAddCommMonoid` `Finset.Icc` `PartialOrder.toPreorder` `instPartialOrder` `instLocallyFiniteOrder` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`Finset.sum_fin_Icc_eq_sum_nat_Icc` `Finset.sum_congr` `Order.lt_add_one_iff` `Nat.instNoMaxOrder` `Order.add_one_le_iff` `Finset.mem_Icc` `Finset.sum_Icc_sub`
`sum_Iic_sub` 📖	mathematical	—	`Finset.sum` `AddCommGroup.toAddCommMonoid` `Finset.Iic` `PartialOrder.toPreorder` `instPartialOrder` `instLocallyFiniteOrderBot` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`Finset.sum_ite_mem_eq` `Finset.sum_fin_eq_sum_range` `Finset.sum_congr_of_eq_on_inter` `Order.lt_add_one_iff` `Nat.instNoMaxOrder` `Order.add_one_le_iff` `Finset.mem_range` `Finset.mem_Iic` `Finset.sum_range_sub`

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_Icc_div` 📖	mathematical	—	`prod` `CommGroup.toCommMonoid` `Icc` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	`Ico_add_one_right_eq_Icc` `Nat.instNoMaxOrder` `prod_Ico_div`
`prod_Icc_succ_top` 📖	mathematical	—	`prod` `Icc` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	`Ico_add_one_right_eq_Icc` `Nat.instNoMaxOrder` `prod_Ico_succ_top`
`prod_Ico_add` 📖	mathematical	—	`prod` `Ico` `PartialOrder.toPreorder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`prod_congr` `add_comm` `prod_Ico_add'`
`prod_Ico_add'` 📖	mathematical	—	`prod` `Ico` `PartialOrder.toPreorder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `map_add_right_Ico` `prod_map`
`prod_Ico_add_right_sub_eq` 📖	mathematical	—	`prod` `Ico` `PartialOrder.toPreorder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `prod_congr` `prod_map` `add_tsub_cancel_right`
`prod_Ico_consecutive` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `prod` `Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder`	—	`prod_union` `Ico_disjoint_Ico_consecutive` `Ico_union_Ico_eq_Ico`
`prod_Ico_div` 📖	mathematical	—	`prod` `CommGroup.toCommMonoid` `Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	`prod_Ico_eq_div` `prod_range_div` `div_div_div_cancel_right`
`prod_Ico_div_bot` 📖	mathematical	—	`DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `prod` `CommGroup.toCommMonoid` `Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder`	—	`div_eq_iff_eq_mul'` `prod_eq_prod_Ico_succ_bot`
`prod_Ico_eq_div` 📖	mathematical	—	`prod` `CommGroup.toCommMonoid` `Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `range`	—	`div_eq_mul_inv` `prod_Ico_eq_mul_inv`
`prod_Ico_eq_mul_inv` 📖	mathematical	—	`prod` `CommGroup.toCommMonoid` `Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `range` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	—	`eq_mul_inv_iff_mul_eq` `mul_comm` `prod_range_mul_prod_Ico`
`prod_Ico_eq_prod_range` 📖	mathematical	—	`prod` `Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `range`	—	`Nat.Ico_zero_eq_range` `prod_Ico_add` `Nat.instIsOrderedCancelAddMonoid` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `zero_add` `tsub_add_cancel_of_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `LT.lt.le` `Ico_eq_empty_of_le` `tsub_eq_zero_iff_le` `range_zero` `prod_empty`
`prod_Ico_id_eq_factorial` 📖	mathematical	—	`prod` `Nat.instCommMonoid` `Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `Nat.factorial`	—	`prod_Ico_succ_top` `Nat.factorial_succ` `mul_comm`
`prod_Ico_reflect` 📖	mathematical	—	`prod` `Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder`	—	`add_le_add_iff_right` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `le_trans` `lt_or_ge` `Nat.Ico_image_const_sub_eq_Ico` `prod_image` `tsub_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `tsub_le_tsub_iff_left` `prod_congr` `Ico_eq_empty_of_le`
`prod_Ico_succ_div_top` 📖	mathematical	—	`DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `prod` `CommGroup.toCommMonoid` `Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder`	—	`div_eq_iff_eq_mul` `prod_Ico_succ_top`
`prod_Ico_succ_top` 📖	mathematical	—	`prod` `Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	`insert_Ico_right_eq_Ico_add_one` `Nat.instNoMaxOrder` `prod_insert` `right_notMem_Ico` `mul_comm`
`prod_Ioc_consecutive` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `prod` `Ioc` `Nat.instPreorder` `Nat.instLocallyFiniteOrder`	—	`Ioc_union_Ioc_eq_Ioc` `prod_union` `disjoint_left` `lt_irrefl` `LT.lt.trans_le` `mem_Ioc`
`prod_Ioc_succ_top` 📖	mathematical	—	`prod` `Ioc` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	`prod_Ioc_consecutive` `Nat.Ioc_succ_singleton` `prod_singleton`
`prod_fin_Icc_eq_prod_nat_Icc` 📖	mathematical	—	`prod` `Icc` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Fin.instLocallyFiniteOrder` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	`prod_ite_mem_eq` `prod_fin_eq_prod_range` `prod_congr_of_eq_on_inter`
`prod_range_diag_flip` 📖	mathematical	—	`prod` `range`	—	`prod_sigma'` `prod_nbij'` `Nat.instOrderedSub` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `lt_of_le_of_lt` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `add_tsub_cancel_left`
`prod_range_div_prod_range` 📖	mathematical	—	`DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `prod` `CommGroup.toCommMonoid` `range` `filter`	—	`prod_Ico_eq_div` `ext`
`prod_range_eq_mul_Ico` 📖	mathematical	—	`prod` `range` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder`	—	`prod_eq_prod_Ico_succ_bot` `range_eq_Ico`
`prod_range_mul_prod_Ico` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `prod` `range` `Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder`	—	`prod_Ico_consecutive` `Nat.Ico_zero_eq_range`
`prod_range_reflect` 📖	mathematical	—	`prod` `range`	—	`prod_congr` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `prod_const` `pow_zero` `tsub_zero` `prod_Ico_reflect` `le_rfl` `tsub_self` `Nat.Ico_zero_eq_range`
`prod_range_succ_div_prod` 📖	mathematical	—	`DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `prod` `CommGroup.toCommMonoid` `range`	—	`div_eq_iff_eq_mul'` `prod_range_succ`
`prod_range_succ_div_top` 📖	mathematical	—	`DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `prod` `CommGroup.toCommMonoid` `range`	—	`div_eq_iff_eq_mul` `prod_range_succ`
`sum_Icc_sub` 📖	mathematical	—	`sum` `AddCommGroup.toAddCommMonoid` `Icc` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`Ico_add_one_right_eq_Icc` `Nat.instNoMaxOrder` `sum_Ico_sub`
`sum_Icc_succ_top` 📖	mathematical	—	`sum` `Icc` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`Ico_add_one_right_eq_Icc` `Nat.instNoMaxOrder` `sum_Ico_succ_top`
`sum_Ico_Ico_comm` 📖	mathematical	—	`sum` `Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder`	—	`sum_sigma'` `sum_nbij'`
`sum_Ico_Ico_comm'` 📖	mathematical	—	`sum` `Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder`	—	`sum_sigma'` `sum_nbij'`
`sum_Ico_add` 📖	mathematical	—	`sum` `Ico` `PartialOrder.toPreorder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`sum_congr` `add_comm` `sum_Ico_add'`
`sum_Ico_add'` 📖	mathematical	—	`sum` `Ico` `PartialOrder.toPreorder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `map_add_right_Ico` `sum_map`
`sum_Ico_add_right_sub_eq` 📖	mathematical	—	`sum` `Ico` `PartialOrder.toPreorder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `sum_congr` `map_add_right_Ico` `sum_map` `add_tsub_cancel_right`
`sum_Ico_consecutive` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `sum` `Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder`	—	`sum_union` `Ico_disjoint_Ico_consecutive` `Ico_union_Ico_eq_Ico`
`sum_Ico_eq_add_neg` 📖	mathematical	—	`sum` `AddCommGroup.toAddCommMonoid` `Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `range` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`eq_add_neg_iff_add_eq` `add_comm` `sum_range_add_sum_Ico`
`sum_Ico_eq_sub` 📖	mathematical	—	`sum` `AddCommGroup.toAddCommMonoid` `Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `range`	—	`sub_eq_add_neg` `sum_Ico_eq_add_neg`
`sum_Ico_eq_sum_range` 📖	mathematical	—	`sum` `Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `range`	—	`Nat.Ico_zero_eq_range` `sum_Ico_add` `Nat.instIsOrderedCancelAddMonoid` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `zero_add` `tsub_add_cancel_of_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `LT.lt.le` `not_le` `Ico_eq_empty_of_le` `tsub_eq_zero_iff_le` `range_zero` `sum_empty`
`sum_Ico_reflect` 📖	mathematical	—	`sum` `Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder`	—	`prod_Ico_reflect`
`sum_Ico_sub` 📖	mathematical	—	`sum` `AddCommGroup.toAddCommMonoid` `Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`sum_Ico_eq_sub` `sum_range_sub` `sub_sub_sub_cancel_right`
`sum_Ico_sub_bot` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `sum` `AddCommGroup.toAddCommMonoid` `Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder`	—	`sub_eq_iff_eq_add'` `sum_eq_sum_Ico_succ_bot`
`sum_Ico_succ_sub_top` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `sum` `AddCommGroup.toAddCommMonoid` `Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder`	—	`sub_eq_iff_eq_add` `sum_Ico_succ_top`
`sum_Ico_succ_top` 📖	mathematical	—	`sum` `Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`insert_Ico_right_eq_Ico_add_one` `Nat.instNoMaxOrder` `sum_insert` `right_notMem_Ico` `add_comm`
`sum_Ioc_consecutive` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `sum` `Ioc` `Nat.instPreorder` `Nat.instLocallyFiniteOrder`	—	`Ioc_union_Ioc_eq_Ioc` `sum_union` `disjoint_left` `lt_irrefl` `LT.lt.trans_le` `mem_Ioc`
`sum_Ioc_succ_top` 📖	mathematical	—	`sum` `Ioc` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`sum_Ioc_consecutive` `Nat.Ioc_succ_singleton` `sum_singleton`
`sum_fin_Icc_eq_sum_nat_Icc` 📖	mathematical	—	`sum` `Icc` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Fin.instLocallyFiniteOrder` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`sum_ite_mem_eq` `sum_fin_eq_sum_range` `sum_congr_of_eq_on_inter`
`sum_range_add_sum_Ico` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `sum` `range` `Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder`	—	`sum_Ico_consecutive` `Nat.Ico_zero_eq_range`
`sum_range_diag_flip` 📖	mathematical	—	`sum` `range`	—	`sum_sigma'` `sum_nbij'` `mem_sigma` `mem_range` `lt_tsub_iff_left` `Nat.instOrderedSub` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Sigma.forall` `lt_of_le_of_lt` `le_add_iff_nonneg_right` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `add_tsub_cancel_left`
`sum_range_eq_add_Ico` 📖	mathematical	—	`sum` `range` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder`	—	`sum_eq_sum_Ico_succ_bot` `range_eq_Ico`
`sum_range_id` 📖	mathematical	—	`sum` `Nat.instAddCommMonoid` `range`	—	`sum_range_id_mul_two`
`sum_range_id_mul_two` 📖	mathematical	—	`sum` `Nat.instAddCommMonoid` `range`	—	`sum_range_reflect` `Nat.instAtLeastTwoHAddOfNat` `mul_two` `sum_add_distrib` `sum_congr` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `mem_range` `sum_const` `card_range` `Nat.nsmul_eq_mul`
`sum_range_reflect` 📖	mathematical	—	`sum` `range`	—	`prod_range_reflect`
`sum_range_sub_sum_range` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `sum` `AddCommGroup.toAddCommMonoid` `range` `filter`	—	`sum_Ico_eq_sub` `ext` `mem_Ico` `mem_filter` `mem_range`
`sum_range_succ_sub_sum` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `sum` `AddCommGroup.toAddCommMonoid` `range`	—	`sub_eq_iff_eq_add'` `sum_range_succ`
`sum_range_succ_sub_top` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `sum` `AddCommGroup.toAddCommMonoid` `range`	—	`sub_eq_iff_eq_add` `sum_range_succ`

---

← Back to Index