Documentation Verification Report

Sum

📁 Source: Mathlib/Data/Nat/Choose/Sum.lean

Statistics

Metric	Count
Definitions	0
Theorems `add_pow`, `add_pow'`, `prod_antidiagonal_pow_choose_succ`, `prod_pow_choose_succ`, `sum_antidiagonal_choose_add`, `sum_antidiagonal_choose_succ_mul`, `sum_antidiagonal_choose_succ_nsmul`, `sum_choose_succ_mul`, `sum_choose_succ_nsmul`, `sum_powerset_apply_card`, `sum_powerset_neg_one_pow_card`, `sum_powerset_neg_one_pow_card_of_nonempty`, `alternating_sum_range_choose`, `alternating_sum_range_choose_eq_choose`, `alternating_sum_range_choose_of_ne`, `choose_middle_le_pow`, `four_pow_le_two_mul_add_one_mul_central_binom`, `sum_Icc_choose`, `sum_range_add_choose`, `sum_range_choose`, `sum_range_choose_halfway`, `sum_range_mul_choose`, `sum_range_multichoose`, `add_pow`, `sub_pow`	25
Total	25

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_pow` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Distrib.toAdd` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.range` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.choose`	—	`pow_zero` `tsub_zero` `Nat.instOrderedSub` `one_mul` `Nat.choose_zero_right` `Nat.cast_one` `mul_one` `Nat.choose_succ_self` `Nat.cast_zero` `MulZeroClass.mul_zero` `Finset.mem_range` `Nat.choose_succ_succ` `Nat.cast_add` `mul_add` `Distrib.leftDistribClass` `pow_succ'` `mul_assoc` `eq` `pow_right` `symm` `lt_of_le_of_ne` `Finset.sum_range_succ` `Finset.range_zero` `Finset.sum_empty` `zero_add` `Nat.choose_self` `Finset.sum_range_succ'` `Finset.sum_congr` `Finset.sum_add_distrib` `add_assoc` `add_mul` `Distrib.rightDistribClass` `Finset.mul_sum` `add_zero`
`add_pow'` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Distrib.toAdd` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `Finset.Nat.instHasAntidiagonal` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.choose`	—	`Finset.Nat.sum_antidiagonal_eq_sum_range_succ` `Finset.sum_congr` `nsmul_eq_mul` `Nat.cast_comm` `add_pow`

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_antidiagonal_pow_choose_succ` 📖	mathematical	—	`prod` `HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `Nat.instHasAntidiagonal` `Monoid.toNatPow` `CommMonoid.toMonoid` `Nat.choose` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`prod_congr` `prod_pow_choose_succ` `Nat.instNoMaxOrder` `tsub_add_eq_add_tsub` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Nat.choose_symm`
`prod_pow_choose_succ` 📖	mathematical	—	`prod` `range` `Monoid.toNatPow` `CommMonoid.toMonoid` `Nat.choose` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`prod_range_succ` `prod_range_succ'` `tsub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `Nat.choose_succ_self` `pow_zero` `mul_one` `prod_congr` `tsub_zero` `Nat.choose_zero_right` `pow_one` `pow_add` `prod_mul_distrib` `mul_assoc` `mul_comm`
`sum_antidiagonal_choose_add` 📖	mathematical	—	`sum` `Nat.instAddCommMonoid` `HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `Nat.instHasAntidiagonal` `Nat.choose`	—	`sum_congr` `antidiagonal_zero` `Nat.instCanonicallyOrderedAdd` `sum_singleton` `add_zero` `Nat.choose_self` `Nat.sum_antidiagonal_succ` `Nat.choose_succ_succ` `add_assoc`
`sum_antidiagonal_choose_succ_mul` 📖	mathematical	—	`sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `Nat.instHasAntidiagonal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.choose` `Distrib.toAdd`	—	`sum_congr` `nsmul_eq_mul` `sum_antidiagonal_choose_succ_nsmul`
`sum_antidiagonal_choose_succ_nsmul` 📖	mathematical	—	`sum` `HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `Nat.instHasAntidiagonal` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `Nat.choose` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`sum_congr` `sum_choose_succ_nsmul` `mem_range` `Order.lt_add_one_iff` `Nat.instNoMaxOrder` `tsub_add_eq_add_tsub` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Nat.choose_symm`
`sum_choose_succ_mul` 📖	mathematical	—	`sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.choose` `Distrib.toAdd`	—	`sum_congr` `nsmul_eq_mul` `sum_choose_succ_nsmul`
`sum_choose_succ_nsmul` 📖	mathematical	—	`sum` `range` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `Nat.choose` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`sum_range_succ` `sum_range_succ'` `tsub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `Nat.choose_succ_self` `zero_nsmul` `add_zero` `sum_congr` `tsub_zero` `Nat.choose_zero_right` `one_nsmul` `add_nsmul` `sum_add_distrib` `add_assoc` `add_comm`
`sum_powerset_apply_card` 📖	mathematical	—	`sum` `Finset` `powerset` `card` `range` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `Nat.choose`	—	`sum_fiberwise_of_maps_to` `mem_range` `card_le_card` `mem_powerset` `sum_congr` `card_powersetCard` `sum_const` `powersetCard_eq_filter` `mem_powersetCard`
`sum_powerset_neg_one_pow_card` 📖	mathematical	—	`sum` `Finset` `Int.instAddCommMonoid` `powerset` `Monoid.toNatPow` `Int.instMonoid` `card` `instEmptyCollection` `decidableEq`	—	`sum_powerset_apply_card` `sum_congr` `nsmul_eq_mul'` `Int.alternating_sum_range_choose`
`sum_powerset_neg_one_pow_card_of_nonempty` 📖	mathematical	`Nonempty`	`sum` `Finset` `Int.instAddCommMonoid` `powerset` `Monoid.toNatPow` `Int.instMonoid` `card`	—	`sum_powerset_neg_one_pow_card` `nonempty_iff_ne_empty`

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`alternating_sum_range_choose` 📖	mathematical	—	`Finset.sum` `instAddCommMonoid` `Finset.range` `Monoid.toNatPow` `instMonoid` `Nat.choose`	—	`Finset.sum_congr` `zero_add` `Finset.sum_singleton` `pow_zero` `Nat.choose_self` `Nat.cast_one` `mul_one` `alternating_sum_range_choose_eq_choose` `Nat.choose_succ_self` `Nat.cast_zero` `MulZeroClass.mul_zero`
`alternating_sum_range_choose_eq_choose` 📖	mathematical	—	`Finset.sum` `instAddCommMonoid` `Finset.range` `Monoid.toNatPow` `instMonoid` `Nat.choose`	—	`Finset.sum_congr` `zero_add` `Finset.sum_singleton` `pow_zero` `Nat.choose_zero_right` `Nat.cast_one` `mul_one` `Finset.sum_range_succ` `Nat.choose_succ_succ`
`alternating_sum_range_choose_of_ne` 📖	mathematical	—	`Finset.sum` `instAddCommMonoid` `Finset.range` `Monoid.toNatPow` `instMonoid` `Nat.choose`	—	`alternating_sum_range_choose`

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`choose_middle_le_pow` 📖	mathematical	—	`choose` `Monoid.toNatPow` `instMonoid`	—	`Finset.single_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `Finset.self_mem_range_succ` `sum_range_choose_halfway`
`four_pow_le_two_mul_add_one_mul_central_binom` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid` `choose`	—	`pow_mul` `add_pow` `Finset.sum_congr` `one_pow` `mul_one` `one_mul` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `choose_le_middle` `instAtLeastTwoHAddOfNat` `mul_div_cancel_left₀` `instMulDivCancelClass` `instCharZero` `Finset.sum_const` `Finset.card_range` `nsmul_eq_mul` `cast_add` `cast_mul` `cast_one`
`sum_Icc_choose` 📖	mathematical	—	`Finset.sum` `instAddCommMonoid` `Finset.Icc` `instPreorder` `instLocallyFiniteOrder` `choose`	—	`lt_or_ge` `choose_eq_zero_of_lt` `Finset.Icc_eq_empty_of_lt` `Finset.sum_empty` `le_induction` `Finset.sum_congr` `Finset.Icc_self` `Finset.sum_singleton` `choose_self` `Finset.Ico_insert_right` `Finset.sum_insert` `Finset.Ico_add_one_right_eq_Icc` `instNoMaxOrder` `choose_succ_succ'`
`sum_range_add_choose` 📖	mathematical	—	`Finset.sum` `instAddCommMonoid` `Finset.range` `choose`	—	`sum_Icc_choose` `Finset.range_eq_Ico` `AddRightCancelSemigroup.toIsRightCancelAdd` `Finset.sum_congr` `IsCancelAdd.toIsRightCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `instIsOrderedCancelAddMonoid` `Finset.map_add_right_Ico` `CanonicallyOrderedAdd.toExistsAddOfLE` `instCanonicallyOrderedAdd` `zero_add` `add_right_comm` `Finset.Ico_add_one_right_eq_Icc` `instNoMaxOrder` `Finset.sum_map`
`sum_range_choose` 📖	mathematical	—	`Finset.sum` `instAddCommMonoid` `Finset.range` `choose` `Monoid.toNatPow` `instMonoid`	—	`add_pow` `instAtLeastTwoHAddOfNat` `Finset.sum_congr` `one_pow` `mul_one` `one_mul` `one_add_one_eq_two`
`sum_range_choose_halfway` 📖	mathematical	—	`Finset.sum` `instAddCommMonoid` `Finset.range` `choose` `Monoid.toNatPow` `instMonoid`	—	`Finset.sum_congr` `choose_symm` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Int.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.mul_neg` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Meta.NormNum.isNat_lt_true` `IsStrictOrderedRing.toIsOrderedRing` `Int.instCharZero` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Tactic.Linarith.natCast_nonneg` `cast_add` `cast_mul` `cast_one` `Finset.mem_range` `mul_right_injective₀` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `two_ne_zero` `two_mul` `Finset.range_eq_Ico` `Finset.sum_Ico_reflect` `Finset.sum_range_add_sum_Ico` `sum_range_choose` `pow_succ` `pow_mul` `mul_comm`
`sum_range_mul_choose` 📖	mathematical	—	`Finset.sum` `instAddCommMonoid` `Finset.range` `choose` `Monoid.toNatPow` `instMonoid`	—	`Finset.sum_congr` `zero_add` `Finset.sum_singleton` `choose_self` `mul_one` `zero_tsub` `instCanonicallyOrderedAdd` `instOrderedSub` `pow_zero` `mul_right_inj'` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `two_ne_zero` `instAtLeastTwoHAddOfNat` `two_mul` `Finset.sum_flip` `choose_symm` `Finset.mem_range_succ_iff` `Finset.sum_add_distrib` `add_mul` `Distrib.rightDistribClass` `Finset.mul_sum` `sum_range_choose` `mul_assoc` `mul_comm` `mul_pow_sub_one`
`sum_range_multichoose` 📖	mathematical	—	`Finset.sum` `instAddCommMonoid` `Finset.range` `multichoose` `choose`	—	`Finset.sum_range_succ'` `Finset.sum_congr` `multichoose_zero_succ` `Finset.sum_const_zero` `multichoose_zero_right` `zero_add` `add_zero` `choose_zero_right`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_pow` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.range` `Distrib.toMul` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.choose`	—	`Commute.add_pow` `Commute.all`
`sub_pow` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddMonoidWithOne.toNatCast` `Nat.choose`	—	`sub_eq_add_neg` `add_pow` `Finset.sum_congr` `Finset.mem_range` `pow_add` `Even.neg_pow` `Distrib.rightDistribClass` `Nat.instAtLeastTwoHAddOfNat` `one_pow` `mul_one` `neg_pow` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.pow_prod_atom` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add`

---

← Back to Index