Theorems · Definition · commutative algebra

PowerSeries.substInv

{R : Type u_2} → [inst : CommRing R] → (P : PowerSeries R) → [Invertible ((PowerSeries.coeff 1) P)] → PowerSeries R

Given a power series P = u • X + O(X²) with u invertible, this is the power series Q such that P(Q(X)) = X. See PowerSeries.subst_substInv_right. See also PowerSeries.substInvOfIsUnit for a variant using IsUnit.

Defined in

Mathlib.RingTheory.PowerSeries.Substitution

Cited by

9 results in Mathlib

Foundations

Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingInvertible