Theorem PowerSeries.hasSubst_substInv

Modification history

2026-04-30 12:24

Mathlib/RingTheory/PowerSeries/Substitution.lean

feat(PowerSeries): `substInv` add add a variant assuming `IsUnit` (#37860) …

Deleted PowerSeries.hasSubst_substInv View on Github →

2026-04-08 19:05

Mathlib/RingTheory/PowerSeries/Substitution.lean

feat(RingTheory/PowerSeries): Construction of `Q` such that `P(Q(X)) = X` (#26645) …

Added PowerSeries.hasSubst_substInv View on Github →