Documentation Verification Report

GenFun

📁 Source: Mathlib/Combinatorics/Enumerative/Partition/GenFun.lean

Statistics

Metric	Count
Definitions `genFun`	1
Theorems `coeff_genFun`, `genFun_eq_tprod`, `hasProd_genFun`, `multipliable_genFun`, `summable_genFun_term`, `summable_genFun_term'`, `tendsto_order_genFun_term_atTop_nhds_top`	7
Total	8

Nat.Partition

Definitions

Name	Category	Theorems
`genFun` 📖	CompOp	3 math math: `hasProd_genFun`, `coeff_genFun`, `genFun_eq_tprod`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_genFun` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `PowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `PowerSeries.instModule` `Semiring.toModule` `LinearMap.instFunLike` `PowerSeries.coeff` `genFun` `Finset.sum` `Nat.Partition` `Finset.univ` `instFintype` `Finsupp.prod` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toCommMonoid` `AddEquiv` `Multiset` `Finsupp` `Multiset.instAdd` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `Multiset.toFinsupp` `parts`	—	—
`genFun_eq_tprod` 📖	mathematical	—	`genFun` `tprod` `PowerSeries` `CommSemiring.toCommMonoid` `PowerSeries.instCommSemiring` `PowerSeries.WithPiTopology.instTopologicalSpace` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `PowerSeries.instSemiring` `CommSemiring.toSemiring` `MvPowerSeries.instOne` `tsum` `PowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toSMul` `PowerSeries.instAlgebra` `Algebra.id` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `PowerSeries.X` `SummationFilter.unconditional`	—	`HasProd.tprod_eq` `PowerSeries.WithPiTopology.instT2Space` `SummationFilter.instNeBotUnconditional` `hasProd_genFun`
`hasProd_genFun` 📖	mathematical	—	`HasProd` `PowerSeries` `CommSemiring.toCommMonoid` `PowerSeries.instCommSemiring` `PowerSeries.WithPiTopology.instTopologicalSpace` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `PowerSeries.instSemiring` `CommSemiring.toSemiring` `MvPowerSeries.instOne` `tsum` `PowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toSMul` `PowerSeries.instAlgebra` `Algebra.id` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `PowerSeries.X` `SummationFilter.unconditional` `genFun`	—	`HasProd.eq_1` `PowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto` `tendsto_atTop_of_eventually_const` `AddRightCancelSemigroup.toIsRightCancelAdd` `Finset.prod_map` `Finset.prod_congr` `Finset.mem_of_subset` `coeff_genFun` `PowerSeries.coeff_prod` `Finset.sum_of_injOn` `Function.Injective.injOn` `toFinsuppAntidiag_injective` `Finset.finsuppAntidiag_mono` `HasSubset.Subset.le` `toFinsuppAntidiag_mem_finsuppAntidiag` `Finset.coe_univ` `Set.image_univ`
`multipliable_genFun` 📖	mathematical	—	`Multipliable` `PowerSeries` `CommSemiring.toCommMonoid` `PowerSeries.instCommSemiring` `PowerSeries.WithPiTopology.instTopologicalSpace` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `PowerSeries.instSemiring` `CommSemiring.toSemiring` `MvPowerSeries.instOne` `tsum` `PowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toSMul` `PowerSeries.instAlgebra` `Algebra.id` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `PowerSeries.X` `SummationFilter.unconditional`	—	`HasProd.multipliable` `hasProd_genFun`
`summable_genFun_term` 📖	mathematical	—	`Summable` `PowerSeries` `PowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `PowerSeries.WithPiTopology.instTopologicalSpace` `Algebra.toSMul` `PowerSeries.instSemiring` `PowerSeries.instAlgebra` `Algebra.id` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `PowerSeries.X` `SummationFilter.unconditional`	—	`PowerSeries.WithPiTopology.summable_of_tendsto_order_atTop_nhds_top` `tendsto_order_genFun_term_atTop_nhds_top`
`summable_genFun_term'` 📖	mathematical	—	`Summable` `PowerSeries` `PowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `PowerSeries.WithPiTopology.instTopologicalSpace` `Algebra.toSMul` `PowerSeries.instSemiring` `PowerSeries.instAlgebra` `Algebra.id` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `PowerSeries.X` `SummationFilter.unconditional`	—	`summable_genFun_term`
`tendsto_order_genFun_term_atTop_nhds_top` 📖	mathematical	—	`Filter.Tendsto` `ENat` `PowerSeries.order` `CommSemiring.toSemiring` `PowerSeries` `Algebra.toSMul` `PowerSeries.instSemiring` `PowerSeries.instAlgebra` `Algebra.id` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `PowerSeries.X` `Filter.atTop` `Nat.instPreorder` `nhds` `ENat.instTopologicalSpace` `Top.top` `instTopENat`	—	`ENat.tendsto_nhds_top_iff_natCast_lt` `Filter.eventually_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `PowerSeries.smul_eq_C_mul` `lt_imp_lt_of_le_of_le` `le_refl` `PowerSeries.le_order_mul` `lt_add_of_nonneg_of_lt` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Subsingleton.eq_zero` `PowerSeries.instSubsingleton` `PowerSeries.order_zero` `PowerSeries.order_X_pow` `IsOrderedRing.toZeroLEOneClass`

---

← Back to Index