Catalan

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

Statistics

Metric	Count
Definitions catalanSeries	1
Theorems catalanSeries_coeff, catalanSeries_constantCoeff, catalanSeries_sq_mul_X_add_one	3
Total	4

PowerSeries

Definitions

Name	Category	Theorems
catalanSeries 📖	CompOp	3 math math: catalanSeries_coeff, catalanSeries_constantCoeff, catalanSeries_sq_mul_X_add_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
catalanSeries_coeff 📖	mathematical	—	DFunLike.coe LinearMap Nat.instSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff catalanSeries catalan	—	—
catalanSeries_constantCoeff 📖	mathematical	—	DFunLike.coe RingHom PowerSeries Semiring.toNonAssocSemiring instSemiring Nat.instSemiring RingHom.instFunLike constantCoeff catalanSeries	—	coeff_zero_eq_constantCoeff_apply catalanSeries_coeff catalan_zero
catalanSeries_sq_mul_X_add_one 📖	mathematical	—	PowerSeries Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring Nat.instSemiring MvPowerSeries.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero catalanSeries X MvPowerSeries.instOne	—	ext coeff_zero_eq_constantCoeff map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass catalanSeries_constantCoeff one_pow constantCoeff_X MulZeroClass.mul_zero zero_add catalanSeries_coeff catalan_zero add_comm SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass coeff_one coeff_succ_mul_X sq coeff_mul Finset.sum_congr catalan_succ'

---

← Back to Index