Binomial

📁 Source: Mathlib/RingTheory/Binomial.lean

Statistics

Metric	Count
Definitions `BinomialRing`, `multichoose`, `instBinomialRing`, `multichoose`, `instBinomialRing`, `multichoose`, `instBinomialRingOfModuleNNRat`	7
Theorems `factorial_nsmul_multichoose`, `toIsAddTorsionFree`, `ascPochhammer_smeval_cast`, `ascPochhammer_smeval_eq_eval`, `ascPochhammer_smeval_neg_eq_descPochhammer`, `descPochhammer_smeval_eq_ascPochhammer`, `descPochhammer_smeval_eq_descFactorial`, `add_choose_eq`, `ascPochhammer_succ_succ`, `choose_add_smul_choose`, `choose_eq_nat_choose`, `choose_eq_smul`, `choose_natCast`, `choose_neg`, `choose_neg'`, `choose_one_right`, `choose_one_right'`, `choose_smul_choose`, `choose_succ_succ`, `choose_zero_ite`, `choose_zero_pos`, `choose_zero_right`, `choose_zero_right'`, `choose_zero_succ`, `descPochhammer_eq_factorial_smul_choose`, `descPochhammer_smeval_add`, `descPochhammer_succ_succ_smeval`, `factorial_nsmul_multichoose_eq_ascPochhammer`, `map_choose`, `map_multichoose`, `multichoose_eq`, `multichoose_eq_multichoose`, `multichoose_neg_add`, `multichoose_neg_of_lt`, `multichoose_neg_self`, `multichoose_neg_succ`, `multichoose_one`, `multichoose_one_right`, `multichoose_one_right'`, `multichoose_succ_neg_natCast`, `multichoose_succ_succ`, `multichoose_two`, `multichoose_zero_right`, `multichoose_zero_right'`, `multichoose_zero_succ`, `smeval_ascPochhammer_int_ofNat`, `smeval_ascPochhammer_nat_cast`, `smeval_ascPochhammer_neg_add`, `smeval_ascPochhammer_neg_of_lt`, `smeval_ascPochhammer_self_neg`, `smeval_ascPochhammer_succ_neg`	51
Total	58

BinomialRing

Definitions

Name	Category	Theorems
`multichoose` 📖	CompOp	2 math math: `Ring.multichoose_eq_multichoose`, `factorial_nsmul_multichoose`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`factorial_nsmul_multichoose` 📖	mathematical	—	`AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `Nat.factorial` `multichoose` `Polynomial.smeval` `Nat.instSemiring` `ascPochhammer` `Module.toMulActionWithZero` `AddCommMonoid.toNatModule`	—	—
`toIsAddTorsionFree` 📖	mathematical	—	`IsAddTorsionFree` `AddCommMonoid.toAddMonoid`	—	—

Int

Definitions

Name	Category	Theorems
`instBinomialRing` 📖	CompOp	8 math math: `Ring.multichoose_neg_self`, `Ring.multichoose_neg_succ`, `LaurentSeries.hasseDeriv_coeff`, `LaurentSeries.hasseDeriv_single_add`, `Ring.multichoose_neg_of_lt`, `Ring.multichoose_neg_add`, `PowerSeries.rescale_neg_one_invOneSubPow`, `LaurentSeries.hasseDeriv_single`
`multichoose` 📖	CompOp	—

Nat

Definitions

Name	Category	Theorems
`instBinomialRing` 📖	CompOp	—

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ascPochhammer_smeval_cast` 📖	mathematical	—	`smeval` `ascPochhammer` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Module.toMulActionWithZero` `Nat.instSemiring` `AddCommMonoid.toNatModule`	—	`smeval_one` `one_smul` `ascPochhammer_succ_right` `mul_add` `Distrib.leftDistribClass` `smeval_add` `smeval_mul_X` `NonUnitalNonAssocSemiring.nat_isScalarTower` `smeval_C_mul` `Nat.cast_smul_eq_nsmul` `nsmul_eq_mul`
`ascPochhammer_smeval_eq_eval` 📖	mathematical	—	`smeval` `Nat.instSemiring` `ascPochhammer` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toMulActionWithZero` `AddCommMonoid.toNatModule` `eval`	—	`eval_eq_smeval` `ascPochhammer_smeval_cast` `IsScalarTower.left` `Monoid.PowAssoc`
`ascPochhammer_smeval_neg_eq_descPochhammer` 📖	mathematical	—	`smeval` `Nat.instSemiring` `ascPochhammer` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Module.toMulActionWithZero` `AddCommMonoid.toNatModule` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NonUnitalNonAssocRing.toAddCommGroup` `Units` `Int.instMonoid` `Units.instSMul` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Int.negOnePow` `Ring.toSemiring` `Int.instRing` `descPochhammer` `AddCommGroup.toIntModule`	—	`smeval_one` `npow_zero` `one_smul` `CharP.cast_eq_zero` `CharP.ofCharZero` `Int.instCharZero` `ascPochhammer_succ_right` `smeval_mul` `NonUnitalNonAssocSemiring.nat_isScalarTower` `AddMonoid.nat_smulCommClass` `descPochhammer_succ_right` `sub_eq_add_neg` `NonUnitalNonAssocRing.int_isScalarTower` `AddGroup.int_smulCommClass` `add_comm` `smeval_add` `smeval_natCast` `nsmul_eq_mul` `mul_one` `smeval_X` `npow_one` `smeval_neg` `neg_add_rev` `neg_neg` `neg_mul_comm` `Int.negOnePow_succ` `Units.neg_smul` `Units.smul_def` `smul_mul_assoc` `neg_mul`
`descPochhammer_smeval_eq_ascPochhammer` 📖	mathematical	—	`smeval` `Ring.toSemiring` `Int.instRing` `descPochhammer` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Module.toMulActionWithZero` `AddCommGroup.toIntModule` `NonUnitalNonAssocRing.toAddCommGroup` `Nat.instSemiring` `ascPochhammer` `AddCommMonoid.toNatModule` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `AddMonoidWithOne.toOne`	—	`smeval_one` `npow_zero` `Nat.cast_succ` `sub_add` `add_sub_cancel_right` `descPochhammer_succ_right` `smeval_mul` `NonUnitalNonAssocRing.int_isScalarTower` `AddGroup.int_smulCommClass` `ascPochhammer_succ_left` `X_mul` `smeval_mul_X` `NonUnitalNonAssocSemiring.nat_isScalarTower` `smeval_comp` `AddMonoid.nat_smulCommClass` `smeval_sub` `C_eq_natCast` `smeval_add` `smeval_C` `smeval_X` `npow_one` `zsmul_one` `Int.cast_natCast` `one_smul`
`descPochhammer_smeval_eq_descFactorial` 📖	mathematical	—	`smeval` `Ring.toSemiring` `Int.instRing` `descPochhammer` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Module.toMulActionWithZero` `AddCommGroup.toIntModule` `NonUnitalNonAssocRing.toAddCommGroup` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Nat.descFactorial`	—	`descPochhammer_zero` `Nat.descFactorial_zero` `Nat.cast_one` `smeval_one` `npow_zero` `one_smul` `descPochhammer_succ_right` `Nat.descFactorial_succ` `smeval_mul` `NonUnitalNonAssocRing.int_isScalarTower` `AddGroup.int_smulCommClass` `mul_comm` `Nat.cast_mul` `smeval_sub` `smeval_X` `smeval_natCast` `npow_one` `nsmul_one` `Nat.descFactorial_eq_zero_iff_lt` `Nat.cast_zero` `MulZeroClass.zero_mul` `Nat.cast_sub`

Ring

Definitions

Name	Category	Theorems
`multichoose` 📖	CompOp	20 math math: `multichoose_two`, `map_multichoose`, `multichoose_neg_self`, `multichoose_neg_succ`, `multichoose_zero_succ`, `multichoose_zero_right`, `factorial_nsmul_multichoose_eq_ascPochhammer`, `multichoose_zero_right'`, `multichoose_eq_multichoose`, `ascPochhammer_succ_succ`, `choose_neg'`, `multichoose_succ_neg_natCast`, `multichoose_eq`, `multichoose_neg_of_lt`, `PadicInt.continuous_multichoose`, `multichoose_one_right'`, `multichoose_one`, `multichoose_succ_succ`, `multichoose_neg_add`, `multichoose_one_right`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_choose_eq` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `toNonAssocRing`	`choose` `NonAssocRing.toAddCommGroupWithOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `toSemiring` `Distrib.toAdd` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `Finset.Nat.instHasAntidiagonal`	—	`BinomialRing.toIsAddTorsionFree` `Nat.factorial_ne_zero` `descPochhammer_eq_factorial_smul_choose` `Monoid.PowAssoc` `Finset.smul_sum` `descPochhammer_smeval_add` `Finset.sum_congr` `Nat.choose_mul_factorial_mul_factorial` `Finset.antidiagonal.fst_le` `Nat.instCanonicallyOrderedAdd` `tsub_eq_of_eq_add_rev` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `List.Nat.mem_antidiagonal` `mul_assoc` `nsmul_eq_mul` `Nat.cast_mul` `Nat.cast_commute`
`ascPochhammer_succ_succ` 📖	mathematical	—	`Polynomial.smeval` `Nat.instSemiring` `ascPochhammer` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Module.toMulActionWithZero` `AddCommMonoid.toNatModule` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `Nat.factorial` `multichoose`	—	`ascPochhammer_succ_right` `ascPochhammer_succ_left` `mul_comm` `Polynomial.smeval_mul` `NonUnitalNonAssocSemiring.nat_isScalarTower` `AddMonoid.nat_smulCommClass` `Polynomial.smeval_add` `Polynomial.smeval_X` `Polynomial.smeval_comp` `Nat.factorial.eq_2` `SemigroupAction.mul_smul` `factorial_nsmul_multichoose_eq_ascPochhammer` `npow_one` `Polynomial.smeval_one` `npow_zero` `one_smul` `Polynomial.C_eq_natCast` `Polynomial.smeval_C` `add_assoc` `add_mul` `Distrib.rightDistribClass` `add_comm` `nsmul_one` `nsmul_eq_mul` `add_rotate'` `succ_nsmul` `one_mul`
`choose_add_smul_choose` 📖	mathematical	—	`AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Nat.choose` `choose` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `AddMonoidWithOne.toNatCast` `Distrib.toMul`	—	`choose_smul_choose` `add_sub_cancel_right`
`choose_eq_nat_choose` 📖	mathematical	—	`choose` `NonAssocRing.toAddCommGroupWithOne` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `Nat.choose`	—	`choose_natCast`
`choose_eq_smul` 📖	mathematical	—	`choose` `NonAssocRing.toAddCommGroupWithOne` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Field.toCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instBinomialRingOfModuleNNRat` `AddCommMonoidWithOne.toAddCommMonoid` `AddCommGroupWithOne.toAddCommMonoidWithOne` `Algebra.toModule` `NNRat` `instCommSemiringNNRat` `DivisionSemiring.toNNRatAlgebra` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Nat.factorial` `Polynomial.smeval` `toSemiring` `Int.instRing` `descPochhammer` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toMulActionWithZero` `AddCommGroup.toIntModule` `toAddCommGroup`	—	`descPochhammer_eq_factorial_smul_choose` `Monoid.PowAssoc` `Nat.cast_smul_eq_nsmul` `inv_smul_smul₀` `Nat.factorial_ne_zero`
`choose_natCast` 📖	mathematical	—	`choose` `NonAssocRing.toAddCommGroupWithOne` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `Nat.choose`	—	`BinomialRing.toIsAddTorsionFree` `Nat.factorial_ne_zero` `descPochhammer_eq_factorial_smul_choose` `nsmul_eq_mul` `Nat.cast_mul` `Nat.descFactorial_eq_factorial_mul_choose` `Polynomial.descPochhammer_smeval_eq_descFactorial`
`choose_neg` 📖	mathematical	—	`choose` `NonAssocRing.toAddCommGroupWithOne` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NonUnitalNonAssocRing.toAddCommGroup` `NonAssocRing.toNonUnitalNonAssocRing` `Units` `Int.instMonoid` `Units.instSMul` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `Int.negOnePow` `SubNegMonoid.toSub` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `AddMonoidWithOne.toOne`	—	`BinomialRing.toIsAddTorsionFree` `Nat.factorial_ne_zero` `descPochhammer_eq_factorial_smul_choose` `SMulCommClass.smul_comm` `AddMonoid.nat_smulCommClass` `Polynomial.descPochhammer_smeval_eq_ascPochhammer` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `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` `Polynomial.ascPochhammer_smeval_neg_eq_descPochhammer`
`choose_neg'` 📖	mathematical	—	`choose` `NonAssocRing.toAddCommGroupWithOne` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NonUnitalNonAssocRing.toAddCommGroup` `NonAssocRing.toNonUnitalNonAssocRing` `Units` `Int.instMonoid` `Units.instSMul` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `Int.negOnePow` `multichoose` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	`choose_neg` `multichoose_eq`
`choose_one_right` 📖	mathematical	—	`choose` `NonAssocRing.toAddCommGroupWithOne`	—	`choose_one_right'` `npow_one`
`choose_one_right'` 📖	mathematical	—	`choose` `NonAssocRing.toAddCommGroupWithOne`	—	`choose.eq_1` `Nat.cast_one` `sub_add_cancel` `multichoose_one_right'`
`choose_smul_choose` 📖	mathematical	—	`AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Nat.choose` `choose` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddMonoidWithOne.toNatCast`	—	`BinomialRing.toIsAddTorsionFree` `Nat.factorial_ne_zero` `nsmul_left_comm` `descPochhammer_eq_factorial_smul_choose` `Nat.choose_mul_factorial_mul_factorial` `smul_mul_smul_comm` `NonUnitalNonAssocSemiring.nat_isScalarTower` `AddCommMonoid.nat_isScalarTower` `AddMonoid.nat_smulCommClass` `mul_nsmul'` `smul_mul_assoc` `add_comm` `descPochhammer_mul` `Polynomial.smeval_mul` `NonUnitalNonAssocRing.int_isScalarTower` `AddGroup.int_smulCommClass` `Polynomial.smeval_comp` `Polynomial.smeval_sub` `Polynomial.smeval_X` `Polynomial.C_eq_natCast` `Polynomial.smeval_C` `npow_one` `npow_zero` `zsmul_one` `Int.cast_natCast` `nsmul_eq_mul`
`choose_succ_succ` 📖	mathematical	—	`choose` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne`	—	`BinomialRing.toIsAddTorsionFree` `Nat.factorial_ne_zero` `smul_add` `Nat.factorial_succ` `SemigroupAction.mul_smul` `descPochhammer_eq_factorial_smul_choose` `descPochhammer_succ_succ_smeval`
`choose_zero_ite` 📖	mathematical	—	`choose` `NonAssocRing.toAddCommGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne`	—	`choose_zero_right` `choose_zero_pos`
`choose_zero_pos` 📖	mathematical	—	`choose` `NonAssocRing.toAddCommGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	—	`choose_zero_succ`
`choose_zero_right` 📖	mathematical	—	`choose` `NonAssocRing.toAddCommGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne`	—	`choose_zero_right'` `npow_zero`
`choose_zero_right'` 📖	mathematical	—	`choose` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne`	—	`BinomialRing.toIsAddTorsionFree` `Nat.factorial_ne_zero` `Nat.cast_zero` `sub_zero` `multichoose_zero_right'` `one_smul`
`choose_zero_succ` 📖	mathematical	—	`choose` `NonAssocRing.toAddCommGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	—	`choose.eq_1` `Nat.cast_succ` `zero_sub` `neg_add` `neg_add_cancel_right` `multichoose_succ_neg_natCast`
`descPochhammer_eq_factorial_smul_choose` 📖	mathematical	—	`Polynomial.smeval` `toSemiring` `Int.instRing` `descPochhammer` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Module.toMulActionWithZero` `AddCommGroup.toIntModule` `NonUnitalNonAssocRing.toAddCommGroup` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Nat.factorial` `choose`	—	`choose.eq_1` `factorial_nsmul_multichoose_eq_ascPochhammer` `descPochhammer_eq_ascPochhammer` `Polynomial.smeval_comp` `NonUnitalNonAssocRing.int_isScalarTower` `AddGroup.int_smulCommClass` `add_comm_sub` `Polynomial.smeval_add` `Polynomial.smeval_X` `npow_one` `Polynomial.C_eq_natCast` `Polynomial.C_1` `Polynomial.C_sub` `Polynomial.smeval_C` `npow_zero` `zsmul_one` `Int.cast_sub` `Int.cast_one` `Int.cast_natCast` `Polynomial.ascPochhammer_smeval_cast`
`descPochhammer_smeval_add` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `toNonAssocRing`	`Polynomial.smeval` `toSemiring` `Int.instRing` `descPochhammer` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toMulActionWithZero` `AddCommGroup.toIntModule` `toAddCommGroup` `Distrib.toAdd` `Finset.sum` `Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `Finset.Nat.instHasAntidiagonal` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `toAddGroupWithOne` `Nat.choose`	—	`Polynomial.smeval_one` `pow_zero` `one_smul` `Finset.sum_congr` `Finset.antidiagonal_zero` `Nat.instCanonicallyOrderedAdd` `Finset.sum_singleton` `Nat.choose_self` `Nat.cast_one` `mul_one` `descPochhammer_succ_right` `mul_comm` `Polynomial.smeval_mul` `Monoid.PowAssoc` `IsScalarTower.right` `Algebra.to_smulCommClass` `Finset.sum_antidiagonal_choose_succ_mul` `Finset.sum_add_distrib` `Polynomial.smeval_sub` `Polynomial.smeval_X` `Polynomial.smeval_natCast` `pow_one` `Finset.mul_sum` `commute_iff_eq` `Polynomial.smeval_commute` `mul_assoc` `Nat.choose_symm_of_eq_add` `List.Nat.mem_antidiagonal` `mul_add` `Distrib.leftDistribClass` `Nat.cast_comm` `add_smul` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.termg_eq` `add_zero` `one_zsmul` `Mathlib.Tactic.Abel.const_add_termg` `add_mul` `Distrib.rightDistribClass`
`descPochhammer_succ_succ_smeval` 📖	mathematical	—	`Polynomial.smeval` `toSemiring` `Int.instRing` `descPochhammer` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Module.toMulActionWithZero` `AddCommGroup.toIntModule` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid`	—	`descPochhammer_succ_left` `descPochhammer_succ_right` `mul_comm` `Polynomial.smeval_mul` `NonUnitalNonAssocRing.int_isScalarTower` `AddGroup.int_smulCommClass` `Polynomial.smeval_X` `npow_one` `Polynomial.smeval_comp` `Polynomial.smeval_sub` `Polynomial.smeval_one` `npow_zero` `one_smul` `add_sub_cancel_right` `add_mul` `Distrib.rightDistribClass` `one_mul` `add_smul` `sub_mul` `Polynomial.C_eq_natCast` `Polynomial.smeval_C` `add_comm` `add_assoc` `add_sub_assoc` `nsmul_eq_mul` `zsmul_one` `Int.cast_natCast` `sub_add_cancel`
`factorial_nsmul_multichoose_eq_ascPochhammer` 📖	mathematical	—	`AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `Nat.factorial` `multichoose` `Polynomial.smeval` `Nat.instSemiring` `ascPochhammer` `Module.toMulActionWithZero` `AddCommMonoid.toNatModule`	—	`BinomialRing.factorial_nsmul_multichoose`
`map_choose` 📖	mathematical	—	`DFunLike.coe` `choose` `NonAssocRing.toAddCommGroupWithOne` `toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `toSemiring`	—	`map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `map_sub` `map_natCast` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `map_multichoose`
`map_multichoose` 📖	mathematical	—	`DFunLike.coe` `multichoose` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `toSemiring`	—	`nsmul_right_injective` `BinomialRing.toIsAddTorsionFree` `Nat.factorial_ne_zero` `IsScalarTower.right` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `factorial_nsmul_multichoose_eq_ascPochhammer` `Polynomial.hom_eval₂` `Unique.instSubsingleton`
`multichoose_eq` 📖	mathematical	—	`multichoose` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `choose` `NonAssocRing.toAddCommGroupWithOne` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `AddMonoidWithOne.toOne`	—	`choose.eq_1` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.isInt_neg` `add_zero` `Mathlib.Tactic.Abel.zero_termg`
`multichoose_eq_multichoose` 📖	mathematical	—	`BinomialRing.multichoose` `multichoose`	—	—
`multichoose_neg_add` 📖	mathematical	—	`multichoose` `Int.instAddCommMonoid` `Monoid.toNatPow` `Int.instMonoid` `Int.instBinomialRing`	—	`Int.instIsAddTorsionFree` `Nat.factorial_ne_zero` `factorial_nsmul_multichoose_eq_ascPochhammer` `smeval_ascPochhammer_neg_add` `smul_zero`
`multichoose_neg_of_lt` 📖	mathematical	—	`multichoose` `Int.instAddCommMonoid` `Monoid.toNatPow` `Int.instMonoid` `Int.instBinomialRing`	—	`Int.instIsAddTorsionFree` `Nat.factorial_ne_zero` `factorial_nsmul_multichoose_eq_ascPochhammer` `smeval_ascPochhammer_neg_of_lt` `smul_zero`
`multichoose_neg_self` 📖	mathematical	—	`multichoose` `Int.instAddCommMonoid` `Monoid.toNatPow` `Int.instMonoid` `Int.instBinomialRing`	—	`Int.instIsAddTorsionFree` `Nat.factorial_ne_zero` `factorial_nsmul_multichoose_eq_ascPochhammer` `smeval_ascPochhammer_self_neg` `nsmul_eq_mul` `Nat.cast_comm`
`multichoose_neg_succ` 📖	mathematical	—	`multichoose` `Int.instAddCommMonoid` `Monoid.toNatPow` `Int.instMonoid` `Int.instBinomialRing`	—	`Int.instIsAddTorsionFree` `Nat.factorial_ne_zero` `factorial_nsmul_multichoose_eq_ascPochhammer` `smeval_ascPochhammer_succ_neg` `smul_zero`
`multichoose_one` 📖	mathematical	—	`multichoose` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`multichoose_zero_right` `zero_add` `multichoose_succ_succ` `multichoose_zero_succ`
`multichoose_one_right` 📖	mathematical	—	`multichoose`	—	`multichoose_one_right'` `npow_one`
`multichoose_one_right'` 📖	mathematical	—	`multichoose`	—	`BinomialRing.toIsAddTorsionFree` `Nat.factorial_ne_zero` `factorial_nsmul_multichoose_eq_ascPochhammer` `ascPochhammer_one` `Polynomial.smeval_X` `Nat.factorial_one` `one_smul`
`multichoose_succ_neg_natCast` 📖	mathematical	—	`multichoose` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NonUnitalNonAssocRing.toAddCommGroup` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`BinomialRing.toIsAddTorsionFree` `Nat.factorial_ne_zero` `smul_zero` `factorial_nsmul_multichoose_eq_ascPochhammer` `Polynomial.smeval_neg_nat` `smeval_ascPochhammer_succ_neg` `Int.cast_zero`
`multichoose_succ_succ` 📖	mathematical	—	`multichoose` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`BinomialRing.toIsAddTorsionFree` `Nat.factorial_ne_zero` `factorial_nsmul_multichoose_eq_ascPochhammer` `smul_add` `add_comm` `ascPochhammer_succ_succ`
`multichoose_two` 📖	mathematical	—	`multichoose` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toOne`	—	`Nat.instAtLeastTwoHAddOfNat` `multichoose_zero_right` `Nat.cast_zero` `zero_add` `one_add_one_eq_two` `multichoose_succ_succ` `multichoose_one` `Nat.cast_succ` `add_comm`
`multichoose_zero_right` 📖	mathematical	—	`multichoose` `MulOne.toOne` `MulOneClass.toMulOne`	—	`multichoose_zero_right'` `npow_zero`
`multichoose_zero_right'` 📖	mathematical	—	`multichoose`	—	`BinomialRing.toIsAddTorsionFree` `Nat.factorial_ne_zero` `factorial_nsmul_multichoose_eq_ascPochhammer` `ascPochhammer_zero` `Polynomial.smeval_one` `Nat.factorial.eq_1`
`multichoose_zero_succ` 📖	mathematical	—	`multichoose` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`BinomialRing.toIsAddTorsionFree` `Nat.factorial_ne_zero` `factorial_nsmul_multichoose_eq_ascPochhammer` `smul_zero` `ascPochhammer_succ_left` `Polynomial.smeval_X_mul` `AddMonoid.nat_smulCommClass` `MulZeroClass.zero_mul`
`smeval_ascPochhammer_int_ofNat` 📖	mathematical	—	`Polynomial.smeval` `Int.instSemiring` `ascPochhammer` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Module.toMulActionWithZero` `AddCommGroup.toIntModule` `NonUnitalNonAssocRing.toAddCommGroup` `Nat.instSemiring` `AddCommMonoid.toNatModule`	—	`Polynomial.smeval_one` `ascPochhammer_succ_right` `Polynomial.smeval_mul` `NonUnitalNonAssocRing.int_isScalarTower` `AddGroup.int_smulCommClass` `NonUnitalNonAssocSemiring.nat_isScalarTower` `AddMonoid.nat_smulCommClass` `Polynomial.smeval_add` `Polynomial.smeval_X` `Polynomial.smeval_C` `natCast_zsmul` `nsmul_eq_mul`
`smeval_ascPochhammer_nat_cast` 📖	mathematical	—	`Polynomial.smeval` `Nat.instSemiring` `ascPochhammer` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Module.toMulActionWithZero` `AddCommMonoid.toNatModule` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.instAddCommMonoid` `Monoid.toNatPow` `Nat.instMonoid` `MonoidWithZero.toMulActionWithZero` `Semiring.toMonoidWithZero`	—	`Polynomial.smeval_at_natCast`
`smeval_ascPochhammer_neg_add` 📖	mathematical	—	`Polynomial.smeval` `Nat.instSemiring` `ascPochhammer` `Int.instAddCommMonoid` `Monoid.toNatPow` `Int.instMonoid` `Module.toMulActionWithZero` `AddCommMonoid.toNatModule`	—	`add_zero` `smeval_ascPochhammer_succ_neg` `ascPochhammer_succ_right` `Polynomial.smeval_mul` `Monoid.PowAssoc` `IsScalarTower.right` `Algebra.to_smulCommClass` `add_assoc` `MulZeroClass.zero_mul`
`smeval_ascPochhammer_neg_of_lt` 📖	mathematical	—	`Polynomial.smeval` `Nat.instSemiring` `ascPochhammer` `Int.instAddCommMonoid` `Monoid.toNatPow` `Int.instMonoid` `Module.toMulActionWithZero` `AddCommMonoid.toNatModule`	—	`smeval_ascPochhammer_neg_add`
`smeval_ascPochhammer_self_neg` 📖	mathematical	—	`Polynomial.smeval` `Nat.instSemiring` `ascPochhammer` `Int.instAddCommMonoid` `Monoid.toNatPow` `Int.instMonoid` `Module.toMulActionWithZero` `AddCommMonoid.toNatModule` `Nat.factorial`	—	`Nat.cast_zero` `neg_zero` `ascPochhammer_zero` `Nat.factorial_zero` `Polynomial.smeval_one` `pow_zero` `one_smul` `Nat.cast_one` `one_mul` `ascPochhammer_succ_left` `Polynomial.smeval_X_mul` `Monoid.PowAssoc` `Algebra.to_smulCommClass` `Polynomial.smeval_comp` `IsScalarTower.right` `Polynomial.smeval_add` `Polynomial.smeval_X` `pow_one` `Nat.cast_add` `neg_add_rev` `neg_add_cancel_comm` `mul_assoc` `mul_comm` `pow_add` `Nat.factorial.eq_2` `Nat.cast_mul` `Nat.cast_succ`
`smeval_ascPochhammer_succ_neg` 📖	mathematical	—	`Polynomial.smeval` `Nat.instSemiring` `ascPochhammer` `Int.instAddCommMonoid` `Monoid.toNatPow` `Int.instMonoid` `Module.toMulActionWithZero` `AddCommMonoid.toNatModule`	—	`ascPochhammer_succ_right` `Polynomial.smeval_mul` `Monoid.PowAssoc` `IsScalarTower.right` `Algebra.to_smulCommClass` `Polynomial.smeval_add` `Polynomial.smeval_X` `Polynomial.C_eq_natCast` `Polynomial.smeval_C` `pow_zero` `pow_one` `Nat.cast_id` `nsmul_eq_mul` `mul_one` `neg_add_cancel` `MulZeroClass.mul_zero`

(root)

Definitions

Name	Category	Theorems
`BinomialRing` 📖	CompData	—
`instBinomialRingOfModuleNNRat` 📖	CompOp	5 math math: `Ring.choose_eq_smul`, `binomialSeries_apply`, `Real.one_div_one_sub_rpow_hasFPowerSeriesOnBall_zero`, `Complex.one_div_one_sub_cpow_hasFPowerSeriesOnBall_zero`, `Complex.ofReal_choose`

---

← Back to Index