Theorem PowerSeries.coeff_X_mul_largeSchroderSeries

Modification history

2026-01-08 08:52
Mathlib/RingTheory/PowerSeries/Schroder.lean
feat(RingTheory/PowerSeries/Schroder): Define the generating function for large Schroder number (#30881) …
Added PowerSeries.coeff_X_mul_largeSchroderSeriesView on Github →