Theorem PowerSeries.constantCoeff_subst_of_constantCoeff_zero

Modification history

2026-08-30 09:00
Mathlib/RingTheory/PowerSeries/Substitution.lean
feat(RingTheory/PowerSeries/Log): log and exp as inverses (#37848) …
Added PowerSeries.constantCoeff_subst_of_constantCoeff_zeroView on Github →