Module

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

Statistics

Metric	Count
Definitions	0
Theorems sum_Ico_by_parts, sum_Ioc_by_parts, sum_range_by_parts	3
Total	3

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sum_Ico_by_parts 📖	mathematical	—	sum AddCommGroup.toAddCommMonoid Ico Nat.instPreorder Nat.instLocallyFiniteOrder 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 SubNegMonoid.toSub range AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	sum_Ico_add' Nat.instIsOrderedCancelAddMonoid CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd sum_congr add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid sum_Ico_sub_bot sum_Ico_succ_sub_top pos_of_gt sub_add_cancel sum_eq_sum_Ico_succ_bot sum_range_succ_sub_sum smul_sub sum_sub_distrib add_sub add_comm sub_smul 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.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat sum_neg_distrib sum_range_succ smul_add Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Abel.zero_termg
sum_Ioc_by_parts 📖	mathematical	—	sum AddCommGroup.toAddCommMonoid Ioc Nat.instPreorder Nat.instLocallyFiniteOrder 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 SubNegMonoid.toSub range AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	sum_congr Nat.instNoMaxOrder sum_Ico_by_parts
sum_range_by_parts 📖	mathematical	—	sum AddCommGroup.toAddCommMonoid range 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 SubNegMonoid.toSub AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	sum_congr zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub smul_zero sub_self range_eq_Ico sum_Ico_by_parts sum_range_zero sub_zero

---

← Back to Index