Interval

📁 Source: Mathlib/Algebra/BigOperators/Group/Finset/Interval.lean

Statistics

Metric	Count
Definitions	0
Theorems prod_Icc_eq_prod_Ico_mul, prod_Icc_of_even_eq_range, prod_Icc_succ_eq_mul_endpoints, prod_Ico_int_div, sum_Icc_eq_sum_Ico_add, sum_Icc_of_even_eq_range, sum_Icc_succ_eq_add_endpoints, sum_Ico_int_sub	8
Total	8

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_Icc_eq_prod_Ico_mul 📖	mathematical	—	prod Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt Int.instLocallyFiniteOrder MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Ico	—	prod_congr right_notMem_Ico Icc_eq_cons_Ico cons_eq_insert prod_insert mul_comm
prod_Icc_of_even_eq_range 📖	mathematical	Function.Even	prod CommGroup.toCommMonoid Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt Int.instLocallyFiniteOrder DivInvMonoid.toDiv Group.toDivInvMonoid CommGroup.toGroup Monoid.toNatPow DivInvMonoid.toMonoid range	—	prod_congr CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero neg_zero Icc_self prod_singleton zero_add sq mul_div_cancel_right Nat.cast_add Nat.cast_one Icc_succ_succ prod_union neg_add_rev covariant_swap_add_of_covariant_add Int.instAddLeftMono IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd prod_pair prod_range_succ pow_two div_mul_eq_mul_div mul_pow Nat.cast_succ
prod_Icc_succ_eq_mul_endpoints 📖	mathematical	—	prod CommGroup.toCommMonoid Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt Int.instLocallyFiniteOrder MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup	—	Icc_succ_succ prod_union Nat.cast_add Nat.cast_one neg_add_rev covariant_swap_add_of_covariant_add Int.instAddLeftMono IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd
prod_Ico_int_div 📖	mathematical	—	prod CommGroup.toCommMonoid Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt Int.instLocallyFiniteOrder DivInvMonoid.toDiv Group.toDivInvMonoid CommGroup.toGroup	—	prod_congr CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero neg_zero Ico_eq_empty_of_le prod_div_distrib div_self' Nat.cast_add_one Ico_succ_succ prod_union neg_add_rev covariant_swap_add_of_covariant_add Int.instAddLeftMono IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le IsRightCancelAdd.addRightStrictMono_of_addRightMono prod_insert prod_singleton mul_assoc mul_div neg_add_cancel_comm mul_comm mul_div_cancel mul_div_cancel_left
sum_Icc_eq_sum_Ico_add 📖	mathematical	—	sum Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt Int.instLocallyFiniteOrder AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Ico	—	sum_congr right_notMem_Ico Icc_eq_cons_Ico cons_eq_insert sum_insert mem_Ico lt_self_iff_false add_comm
sum_Icc_of_even_eq_range 📖	mathematical	Function.Even	sum AddCommGroup.toAddCommMonoid Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt Int.instLocallyFiniteOrder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddMonoid.toNatSMul SubNegMonoid.toAddMonoid range	—	sum_congr CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero neg_zero Icc_self sum_singleton zero_add two_nsmul add_sub_cancel_right Nat.cast_add Nat.cast_one Icc_succ_succ sum_union neg_add_rev disjoint_insert_right mem_Icc le_add_iff_nonneg_left covariant_swap_add_of_covariant_add Int.instAddLeftMono IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le add_neg_le_iff_le_add disjoint_singleton_right add_le_iff_nonpos_right IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd sum_pair sum_range_succ sub_add_eq_add_sub nsmul_add Nat.cast_succ
sum_Icc_succ_eq_add_endpoints 📖	mathematical	—	sum AddCommGroup.toAddCommMonoid Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt Int.instLocallyFiniteOrder AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	Icc_succ_succ sum_union Nat.cast_add Nat.cast_one neg_add_rev disjoint_insert_right mem_Icc le_add_iff_nonneg_left covariant_swap_add_of_covariant_add Int.instAddLeftMono IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le neg_add_le_iff_le_add add_neg_le_iff_le_add disjoint_singleton_right add_le_iff_nonpos_right IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd
sum_Ico_int_sub 📖	mathematical	—	sum AddCommGroup.toAddCommMonoid Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt Int.instLocallyFiniteOrder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	sum_congr CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero neg_zero Ico_eq_empty_of_le le_refl sum_sub_distrib sub_self Nat.cast_add_one Ico_succ_succ sum_union neg_add_rev disjoint_insert_right mem_Ico le_add_iff_nonneg_left covariant_swap_add_of_covariant_add Int.instAddLeftMono IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le add_neg_lt_iff_lt_add IsRightCancelAdd.addRightStrictMono_of_addRightMono disjoint_singleton_right lt_self_iff_false sum_insert sum_singleton add_assoc add_sub neg_add_cancel_comm add_comm add_sub_cancel add_sub_cancel_left

---

← Back to Index