Theorem PowerSeries.HasSubst.exp_sub_one

Modification history

2026-04-09 09:56
Mathlib/RingTheory/PowerSeries/Log.lean
feat(PowerSeries): add barebones Log.lean (#36329)
Added PowerSeries.HasSubst.exp_sub_oneView on Github →