Documentation Verification Report

Binomial

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

Statistics

Metric	Count
Definitions `binomialFamily`, `instPowSubtypeUnitsMemSubgroupOrderTopSubOnePos`	2
Theorems `binomialFamily_apply`, `binomialFamily_apply_of_orderTop_nonpos`, `binomialFamily_mem_support`, `binomialFamily_orderTop_pos`, `orderTop_hsum_binomialFamily_pos`, `binomial_power`, `coeff_toOrderTopSubOnePos_pow`, `pow_add`	8
Total	10

HahnSeries

Definitions

Name	Category	Theorems
`instPowSubtypeUnitsMemSubgroupOrderTopSubOnePos` 📖	CompOp	3 math math: `binomial_power`, `pow_add`, `coeff_toOrderTopSubOnePos_pow`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`binomial_power` 📖	mathematical	—	`Units` `HahnSeries` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `orderTopSubOnePos` `instPowSubtypeUnitsMemSubgroupOrderTopSubOnePos` `toOrderTopSubOnePos` `SummableFamily.hsum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `SummableFamily.binomialFamily` `Algebra.id` `Units.val` `SummableFamily.orderTop_hsum_binomialFamily_pos`	—	—
`coeff_toOrderTopSubOnePos_pow` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Units.val` `HahnSeries` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Units` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `orderTopSubOnePos` `instPowSubtypeUnitsMemSubgroupOrderTopSubOnePos` `toOrderTopSubOnePos` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `instAdd` `SubNegMonoid.toAddMonoid` `SubNegZeroMonoid.toSubNegMonoid` `instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DFunLike.coe` `ZeroHom` `instZero` `ZeroHom.funLike` `single` `orderTop_sub_pos` `AddMonoid.toNatSMul` `Algebra.toSMul` `Algebra.id` `Ring.choose` `NonAssocRing.toAddCommGroupWithOne` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Monoid.toNatPow`	—	`orderTop_sub_pos` `finsum_eq_single` `SummableFamily.binomialFamily_apply` `map_zero` `ZeroHom.zeroHomClass` `add_zero` `sub_self` `orderTop_zero` `add_sub_cancel_left` `orderTop_single` `coeff_smul` `single_pow` `coeff_single_of_ne` `Mathlib.Tactic.Contrapose.contrapose₄` `StrictMono.injective` `nsmul_left_strictMono` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `smul_zero` `coeff_single_same` `smul_eq_mul`
`pow_add` 📖	mathematical	—	`Units` `HahnSeries` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `orderTopSubOnePos` `instPowSubtypeUnitsMemSubgroupOrderTopSubOnePos` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Subgroup.mul`	—	`SummableFamily.orderTop_hsum_binomialFamily_pos` `SummableFamily.powerSeriesFamily.congr_simp` `PowerSeries.binomialSeries_add` `SummableFamily.hsum_powerSeriesFamily_mul` `SummableFamily.hsum_mul` `toOrderTopSubOnePos.congr_simp` `SetLike.coe_eq_coe`

HahnSeries.SummableFamily

Definitions

Name	Category	Theorems
`binomialFamily` 📖	CompOp	5 math math: `binomialFamily_orderTop_pos`, `binomialFamily_apply_of_orderTop_nonpos`, `orderTop_hsum_binomialFamily_pos`, `HahnSeries.binomial_power`, `binomialFamily_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`binomialFamily_apply` 📖	mathematical	`WithTop` `Preorder.toLT` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `WithTop.zero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `HahnSeries.orderTop` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `HahnSeries` `HahnSeries.instSub` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `HahnSeries.instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	`DFunLike.coe` `HahnSeries.SummableFamily` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instFunLike` `binomialFamily` `HahnSeries.instSMul` `DistribSMul.toSMulZeroClass` `AddMonoidWithOne.toAddMonoid` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `Algebra.toModule` `Ring.choose` `NonAssocRing.toAddCommGroupWithOne` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Monoid.toNatPow` `HahnSeries.instSemiring`	—	`PowerSeries.binomialSeries_coeff` `smul_assoc` `HahnModule.instIsScalarTowerHahnSeries` `IsScalarTower.right` `one_smul`
`binomialFamily_apply_of_orderTop_nonpos` 📖	mathematical	`WithTop` `Preorder.toLT` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `WithTop.zero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `HahnSeries.orderTop` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `HahnSeries` `HahnSeries.instSub` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `HahnSeries.instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	`DFunLike.coe` `HahnSeries.SummableFamily` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instFunLike` `binomialFamily` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `HahnSeries.instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `HahnSeries.instZero`	—	`binomialFamily.eq_1` `powerSeriesFamily_of_not_orderTop_pos` `PowerSeries.binomialSeries_coeff` `Ring.choose_zero_right'` `pow_zero` `one_smul` `powers_zero` `Pi.single_eq_same` `Pi.single_eq_of_ne` `smul_zero` `zero_pow`
`binomialFamily_mem_support` 📖	mathematical	`WithTop` `Preorder.toLT` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `WithTop.zero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `HahnSeries.orderTop` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `HahnSeries` `HahnSeries.instSub` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `HahnSeries.instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Set` `Set.instMembership` `HahnSeries.support` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DFunLike.coe` `HahnSeries.SummableFamily` `instFunLike` `binomialFamily`	`Preorder.toLE`	—	`binomialFamily_apply` `Ring.choose_zero_right'` `pow_zero` `one_smul` `HahnSeries.coeff_one` `le_of_lt` `WithTop.coe_pos` `lt_of_lt_of_le` `binomialFamily_orderTop_pos` `HahnSeries.orderTop_le_of_coeff_ne_zero`
`binomialFamily_orderTop_pos` 📖	mathematical	`WithTop` `Preorder.toLT` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `WithTop.zero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `HahnSeries.orderTop` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `HahnSeries` `HahnSeries.instSub` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `HahnSeries.instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	`NonUnitalNonAssocSemiring.toAddCommMonoid` `DFunLike.coe` `HahnSeries.SummableFamily` `instFunLike` `binomialFamily`	—	`PowerSeries.binomialSeries_coeff` `smul_assoc` `HahnModule.instIsScalarTowerHahnSeries` `IsScalarTower.right` `one_smul` `nsmul_pos_iff` `WithTop.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `HahnSeries.orderTop_nsmul_le_orderTop_pow` `HahnSeries.orderTop_le_orderTop_smul`
`orderTop_hsum_binomialFamily_pos` 📖	mathematical	`WithTop` `Preorder.toLT` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `WithTop.zero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `HahnSeries.orderTop` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `HahnSeries` `HahnSeries.instSub` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `HahnSeries.instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	`NonUnitalNonAssocSemiring.toAddCommMonoid` `hsum` `binomialFamily`	—	`subsingleton_or_nontrivial` `Subsingleton.eq_zero` `HahnSeries.instSubsingleton` `HahnSeries.orderTop_of_subsingleton` `HahnSeries.orderTop_self_sub_one_pos_iff` `hsum_orderTop_of_le` `binomialFamily_apply` `Ring.choose_zero_right'` `pow_zero` `one_smul` `HahnSeries.orderTop_one` `NeZero.one` `binomialFamily_mem_support` `HahnSeries.coeff_eq_zero_of_lt_orderTop` `binomialFamily_orderTop_pos` `HahnSeries.coeff_one` `hsum_leadingCoeff_of_le`

---

← Back to Index