Documentation Verification Report

Binomial

📁 Source: Mathlib/RingTheory/PowerSeries/Binomial.lean

Statistics

Metric	Count
Definitions `binomialSeries`	1
Theorems `binomialSeries_add`, `binomialSeries_coeff`, `binomialSeries_constantCoeff`, `binomialSeries_nat`, `binomialSeries_zero`, `rescale_neg_one_invOneSubPow`	6
Total	7

PowerSeries

Definitions

Name	Category	Theorems
`binomialSeries` 📖	CompOp	6 math math: `binomialSeries_coeff`, `binomialSeries_add`, `binomialSeries_zero`, `binomialSeries_nat`, `binomialSeries_constantCoeff`, `rescale_neg_one_invOneSubPow`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`binomialSeries_add` 📖	mathematical	—	`binomialSeries` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Algebra.toSMul` `CommRing.toCommSemiring` `Ring.toSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `PowerSeries` `MvPowerSeries.instMul`	—	`ext` `binomialSeries_coeff` `Ring.add_choose_eq` `Commute.all` `Finset.sum_smul` `coeff_mul` `Finset.sum_congr` `Algebra.mul_smul_comm` `mul_one` `mul_comm` `SemigroupAction.mul_smul`
`binomialSeries_coeff` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `binomialSeries` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Ring.choose` `NonAssocRing.toAddCommGroupWithOne` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	—
`binomialSeries_constantCoeff` 📖	mathematical	—	`DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `Ring.toSemiring` `RingHom.instFunLike` `constantCoeff` `binomialSeries` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Algebra.toSMul` `CommRing.toCommSemiring`	—	`binomialSeries_coeff` `Ring.choose_zero_right'` `pow_zero` `one_smul`
`binomialSeries_nat` 📖	mathematical	—	`binomialSeries` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Algebra.toSMul` `CommRing.toCommSemiring` `Ring.toSemiring` `AddMonoidWithOne.toNatCast` `CommRing.toRing` `PowerSeries` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRing` `MvPowerSeries.instOne` `X`	—	`ext` `Polynomial.coe_pow` `Polynomial.coe_add` `Polynomial.coe_one` `Polynomial.coe_X` `Polynomial.coeff_coe` `binomialSeries_coeff` `Polynomial.coeff_one_add_X_pow` `Ring.choose_natCast` `Monoid.PowAssoc` `Nat.cast_smul_eq_nsmul` `nsmul_eq_mul` `mul_one`
`binomialSeries_zero` 📖	mathematical	—	`binomialSeries` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Algebra.toSMul` `CommRing.toCommSemiring` `Ring.toSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `PowerSeries` `MvPowerSeries.instOne`	—	`Nat.cast_zero` `pow_zero` `binomialSeries_nat`
`rescale_neg_one_invOneSubPow` 📖	mathematical	—	`DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `rescale` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `invOneSubPow` `binomialSeries` `Int.instCommRing` `Int.instBinomialRing` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup`	—	`ext` `coeff_rescale` `binomialSeries_coeff` `Int.cast_negOnePow_natCast` `zsmul_eq_mul` `CharP.cast_eq_zero` `CharP.ofCharZero` `Int.instCharZero` `coeff_one` `one_smul` `neg_zero` `Ring.choose_zero_right'` `zero_add` `pow_zero` `smul_zero` `Ring.choose_zero_ite` `Monoid.PowAssoc` `zero_smul` `Nat.cast_add` `Nat.cast_one` `neg_add_rev` `mul_one` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_neg` `Mathlib.Tactic.Abel.term_add_constg` `Mathlib.Tactic.Abel.const_add_termg` `add_zero` `Ring.choose_neg` `Nat.choose_symm_add` `Units.smul_def` `Ring.choose_natCast` `Int.cast_natCast` `Int.cast_mul`

---

← Back to Index