Commit 2026-01-08 08:52 618702d2

View on Github →

feat(RingTheory/PowerSeries/Schroder): Define the generating function for large Schroder number (#30881) Define the generating function for large Schroder number. Main result : Prove some lemmas and the generating function of large Schroder. Todo : Prove the generating function of small Schroder.

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/PowerSeries/Schroder.lean

added theorem PowerSeries.coeff_X_mul_largeSchroderSeries

added theorem PowerSeries.coeff_X_mul_largeSchroderSeriesSeries_sq

added theorem PowerSeries.coeff_largeSchroderSeries

added theorem PowerSeries.constantCoeff_largeSchroderSeries

added def PowerSeries.largeSchroderSeries

added theorem PowerSeries.largeSchroderSeries_eq_one_add_X_mul_largeSchroderSeries_add_X_mul_largeSchroderSeries_sq