Intervals

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

Statistics

Metric	Count
Definitions	0
Theorems 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_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_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_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	49
Total	49

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
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	—	IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd map_add_right_Ico prod_map
prod_Ico_add_right_sub_eq 📖	mathematical	—	prod Ico PartialOrder.toPreorder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd prod_congr prod_map add_tsub_cancel_right IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toAddLeftReflectLT
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 AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add 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 IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd 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_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 AddLeftCancelSemigroup.toIsLeftCancelAdd 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_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	—	IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd map_add_right_Ico sum_map
sum_Ico_add_right_sub_eq 📖	mathematical	—	sum Ico PartialOrder.toPreorder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd sum_congr map_add_right_Ico sum_map add_tsub_cancel_right IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toAddLeftReflectLT
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_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 AddLeftCancelSemigroup.toIsLeftCancelAdd 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