Commit 2026-08-30 09:00 6c8d0ef0

feat(RingTheory/PowerSeries/Log): log and exp as inverses (#37848) This adds the lemmas in Log.lean

• PowerSeries.derivative_log_mul_one_add_X: (log(1+X))' · (1 + X) = 1.
• PowerSeries.subst_exp_log: exp and log are mutually inverse: substituting log(1+X) into exp yields 1 + X.
• PowerSeries.subst_log_exp_sub_one: Substituting exp X - 1 into log(1+X) yields X.
• PowerSeries.logOf_exp: The reformulation logOf (exp X) = X, where logOf f is log(1+X) evaluated at f - 1. It also addsmk_neg_one_pow_mul_one_add_eq_one to WellKnown.lean and improves Substitution.lean. Note: I'm using Claude + Opus for supervised formalization tasks. Claude has no permission to use git on my machine.

• depends on: #40571