Commit 2026-04-14 12:34 2233275c

View on Github →

chore: golf proofs in Mathlib/RingTheory/PowerSeries/Substitution.lean (#37821) This PR golfs three proofs in Mathlib/RingTheory/PowerSeries/Substitution.lean by reusing existing lemmas instead of reproving the relevant coefficient computations. Specifically:

  • constantCoeff_subst_eq_zero now uses MvPowerSeries.constantCoeff_subst_eq_zero.
  • Polynomial.toPowerSeries_toMvPowerSeries now uses Polynomial.pUnitAlgEquiv_symm_toPowerSeries.
  • map_subst now uses MvPowerSeries.map_subst. This is a pure proof cleanup; no declarations are changed.

Estimated changes