theorem HexTruncatedSeriesTheory.ofPowerSeries_invOfUnit {R : Type u} {n : ℕ} [CommRing R] (f : PowerSeries R) (u : Rˣ) (hu : PowerSeries.constantCoeff f = ↑u) : ofPowerSeries (f.invOfUnit u) = (ofPowerSeries f).invOfUnit ↑u⁻¹

Truncation carries Mathlib's unit-certified inverse to executable Newton inversion.

theorem HexTruncatedSeriesTheory.ofPowerSeries_subst {R : Type u} {n : ℕ} [CommRing R] (f g : PowerSeries R) (hg : PowerSeries.constantCoeff g = 0) : ofPowerSeries (PowerSeries.subst g f) = (ofPowerSeries f).comp (ofPowerSeries g)

Truncation carries Mathlib substitution by a zero-constant series to executable composition.

theorem HexTruncatedSeriesTheory.ofPowerSeries_substInvOfIsUnit {R : Type u} {n : ℕ} [CommRing R] (g : PowerSeries R) (h0 : PowerSeries.constantCoeff g = 0) (hu : IsUnit ((PowerSeries.coeff 1) g)) : ofPowerSeries (g.substInvOfIsUnit hu) = (ofPowerSeries g).revOfUnit ↑hu.unit⁻¹

Truncation carries Mathlib's compositional inverse to executable Newton reversion.

theorem HexTruncatedSeriesTheory.ofPowerSeries_exp {R : Type u} {n : ℕ} [CommRing R] [Algebra ℚ R] [Hex.TSeries.NatInverses R (n - 1)] (f : PowerSeries R) (h : PowerSeries.constantCoeff f = 0) : ofPowerSeries (PowerSeries.subst f (PowerSeries.exp R)) = (ofPowerSeries f).exp

Truncation carries Mathlib's formal exponential to the executable truncated exponential.

theorem HexTruncatedSeriesTheory.ofPowerSeries_logOf {R : Type u} {n : ℕ} [CommRing R] [Algebra ℚ R] [Hex.TSeries.NatInverses R (n - 1)] (f : PowerSeries R) (h : PowerSeries.constantCoeff f = 1) : ofPowerSeries f.logOf = (ofPowerSeries f).log

Truncation carries Mathlib's formal logarithm to the executable truncated logarithm.

theorem HexTruncatedSeriesTheory.exists_unique_sq {R : Type u} [CommRing R] (f : PowerSeries R) (r : R) (hr : r * r = PowerSeries.constantCoeff f) (hu : IsUnit (2 * r)) : ∃! s : PowerSeries R, s * s = f ∧ PowerSeries.constantCoeff s = r

A unit derivative at a chosen constant root gives exactly one square-root lift in the full power-series ring.