Commit 2026-04-09 09:56 08f1264b

View on Github →

feat(PowerSeries): add barebones Log.lean (#36329)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/PowerSeries/Basic.lean

added theorem PowerSeries.constantCoeff_eq

Modified Mathlib/RingTheory/PowerSeries/Derivative.lean

Modified Mathlib/RingTheory/PowerSeries/Exp.lean

Created Mathlib/RingTheory/PowerSeries/Log.lean

added theorem PowerSeries.HasSubst.exp_sub_one

added theorem PowerSeries.HasSubst.log

added theorem PowerSeries.coeff_log

added theorem PowerSeries.coeff_one_log

added theorem PowerSeries.constantCoeff_log

added theorem PowerSeries.constantCoeff_logOf

added theorem PowerSeries.deriv_log

added def PowerSeries.log

added theorem PowerSeries.logOf_eq

added theorem PowerSeries.logOf_one_add_X

added theorem PowerSeries.map_log

added theorem PowerSeries.order_log

Modified Mathlib/RingTheory/PowerSeries/Substitution.lean

added theorem PowerSeries.X_subst