Glaisher

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

Statistics

Metric	Count
Definitions	0
Theorems card_odds_eq_card_distincts, card_restricted_eq_card_countRestricted, hasProd_powerSeriesMk_card_countRestricted, hasProd_powerSeriesMk_card_restricted, multipliable_powerSeriesMk_card_countRestricted, multipliable_powerSeriesMk_card_restricted, powerSeriesMk_card_countRestricted_eq_tprod, powerSeriesMk_card_restricted_eq_powerSeriesMk_card_countRestricted, powerSeriesMk_card_restricted_eq_tprod	9
Total	9

Nat.Partition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_odds_eq_card_distincts 📖	mathematical	—	Finset.card Nat.Partition odds distincts	—	Nat.instAtLeastTwoHAddOfNat restricted.congr_simp card_restricted_eq_card_countRestricted Mathlib.Meta.NormNum.isNat_lt_true IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instCharZero Mathlib.Meta.NormNum.isNat_ofNat
card_restricted_eq_card_countRestricted 📖	mathematical	—	Finset.card Nat.Partition restricted countRestricted	—	Int.instCharZero PowerSeries.ext_iff powerSeriesMk_card_restricted_eq_powerSeriesMk_card_countRestricted IsStrictOrderedRing.noZeroDivisors Int.instIsStrictOrderedRing AddGroup.existsAddOfLE
hasProd_powerSeriesMk_card_countRestricted 📖	mathematical	—	HasProd PowerSeries CommSemiring.toCommMonoid PowerSeries.instCommSemiring PowerSeries.WithPiTopology.instTopologicalSpace Finset.sum PowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finset.range Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero PowerSeries.instSemiring PowerSeries.X AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finset.card Nat.Partition countRestricted SummationFilter.unconditional	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Finset.sum_congr Subsingleton.eq_one PowerSeries.instSubsingleton one_pow Finset.sum_range_eq_add_Ico Finset.sum_Ico_eq_sum_range MulZeroClass.mul_zero pow_zero add_comm one_smul tsum_eq_sum SummationFilter.instLeAtTopUnconditional smul_eq_zero_of_left NeZero.one Nat.instOrderedSub Finset.card_filter Finset.prod_congr Finset.prod_boole Finset.sum_boole hasProd_genFun
hasProd_powerSeriesMk_card_restricted 📖	mathematical	—	HasProd PowerSeries CommSemiring.toCommMonoid PowerSeries.instCommSemiring PowerSeries.WithPiTopology.instTopologicalSpace tsum PowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero PowerSeries.instSemiring PowerSeries.X SummationFilter.unconditional MvPowerSeries.instOne AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finset.card Nat.Partition restricted	—	tsum_eq_zero_add' PowerSeries.WithPiTopology.instT2Space IsTopologicalSemiring.toContinuousAdd PowerSeries.WithPiTopology.instIsTopologicalSemiring pow_mul pow_add Summable.mul_right PowerSeries.WithPiTopology.summable_pow_of_constantCoeff_eq_zero pow_one map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass PowerSeries.constantCoeff_X MulZeroClass.mul_zero pow_zero one_smul zero_smul tsum_zero add_zero Finset.card_filter Finset.sum_congr Finset.prod_congr Finset.prod_boole Finset.sum_boole hasProd_genFun
multipliable_powerSeriesMk_card_countRestricted 📖	mathematical	—	Multipliable PowerSeries CommSemiring.toCommMonoid PowerSeries.instCommSemiring PowerSeries.WithPiTopology.instTopologicalSpace Finset.sum PowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finset.range Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero PowerSeries.instSemiring PowerSeries.X SummationFilter.unconditional	—	multipliable_of_exists_eq_zero SummationFilter.instLeAtTopUnconditional HasProd.multipliable hasProd_powerSeriesMk_card_countRestricted
multipliable_powerSeriesMk_card_restricted 📖	mathematical	—	Multipliable PowerSeries CommSemiring.toCommMonoid PowerSeries.instCommSemiring PowerSeries.WithPiTopology.instTopologicalSpace tsum PowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero PowerSeries.instSemiring PowerSeries.X SummationFilter.unconditional MvPowerSeries.instOne	—	HasProd.multipliable hasProd_powerSeriesMk_card_restricted
powerSeriesMk_card_countRestricted_eq_tprod 📖	mathematical	—	AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring Finset.card Nat.Partition countRestricted tprod PowerSeries CommSemiring.toCommMonoid PowerSeries.instCommSemiring PowerSeries.WithPiTopology.instTopologicalSpace Finset.sum PowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Finset.range Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero PowerSeries.instSemiring PowerSeries.X SummationFilter.unconditional	—	HasProd.tprod_eq PowerSeries.WithPiTopology.instT2Space SummationFilter.instNeBotUnconditional hasProd_powerSeriesMk_card_countRestricted
powerSeriesMk_card_restricted_eq_powerSeriesMk_card_countRestricted 📖	mathematical	—	AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Finset.card Nat.Partition restricted countRestricted	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim PowerSeries.instSubsingleton powerSeriesMk_card_restricted_eq_tprod T25Space.t2Space T3Space.t25Space instT3Space T1Space.t0Space instT1SpaceOfDiscreteTopology IsTopologicalAddGroup.regularSpace IsTopologicalRing.to_topologicalAddGroup DiscreteTopology.topologicalRing IsTopologicalRing.toIsTopologicalSemiring powerSeriesMk_card_countRestricted_eq_tprod mul_right_cancel₀ IsCancelMulZero.toIsRightCancelMulZero NoZeroDivisors.to_isCancelMulZero PowerSeries.instNoZeroDivisors PowerSeries.WithPiTopology.tprod_one_sub_X_pow_ne_zero Multipliable.tprod_mul PowerSeries.WithPiTopology.instT2Space IsTopologicalSemiring.toContinuousMul PowerSeries.WithPiTopology.instIsTopologicalSemiring SummationFilter.instNeBotUnconditional multipliable_powerSeriesMk_card_countRestricted PowerSeries.WithPiTopology.multipliable_one_sub_X_pow tprod_congr pow_mul Finset.sum_congr geom_sum_mul_neg
powerSeriesMk_card_restricted_eq_tprod 📖	mathematical	—	AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring Finset.card Nat.Partition restricted tprod PowerSeries CommSemiring.toCommMonoid PowerSeries.instCommSemiring PowerSeries.WithPiTopology.instTopologicalSpace tsum PowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero PowerSeries.instSemiring PowerSeries.X SummationFilter.unconditional MvPowerSeries.instOne	—	HasProd.tprod_eq PowerSeries.WithPiTopology.instT2Space SummationFilter.instNeBotUnconditional hasProd_powerSeriesMk_card_restricted

---

← Back to Index