Commit 2026-04-30 12:24 11568e6e

View on Github →

feat(PowerSeries): substInv add add a variant assuming IsUnit (#37860) In this PR, I add a variant assuming IsUnit in substInv.

Estimated changes

Modified Mathlib/RingTheory/PowerSeries/Substitution.lean

added theorem PowerSeries.HasSubst.substInv

added theorem PowerSeries.HasSubst.substInvOfIsUnit

added theorem PowerSeries.coeff_one_substInvOfIsUnit

added theorem PowerSeries.constantCoeff_substInvOfIsUnit

deleted theorem PowerSeries.hasSubst_substInv

added def PowerSeries.substInvOfIsUnit

added theorem PowerSeries.substInvOfIsUnit_eq_substInv

added theorem PowerSeries.subst_substInvOfIsUnit_left

added theorem PowerSeries.subst_substInvOfIsUnit_right