theorem HexTruncatedSeriesTheory.pow_eq_mathlib {R : Type u} {n : ℕ} [CommRing R] (a : Hex.TSeries R n) (k : ℕ) : a.pow k = NPow.npow k a

The executable square-and-multiply power agrees with Mathlib's recursive monoid power. This bridges the standalone Pow instance in the Mathlib-free layer with the npow field supplied by commRing.

@[simp]

theorem HexTruncatedSeriesTheory.ofPowerSeries_pow {R : Type u} {n : ℕ} [CommRing R] (f : PowerSeries R) (k : ℕ) : ofPowerSeries (f ^ k) = (ofPowerSeries f).pow k

Truncation carries Mathlib powers to the executable square-and-multiply power.

@[simp]

theorem HexTruncatedSeriesTheory.ofPowerSeries_C {R : Type u} {n : ℕ} [CommRing R] (r : R) : ofPowerSeries (PowerSeries.C r) = Hex.TSeries.C r

Truncating Mathlib's constant series gives the executable constant series.

@[simp]

theorem HexTruncatedSeriesTheory.ofPowerSeries_X {R : Type u} {n : ℕ} [CommRing R] : ofPowerSeries PowerSeries.X = Hex.TSeries.X

Truncating Mathlib's variable gives the executable variable.

@[simp]

theorem HexTruncatedSeriesTheory.truncate_ofPowerSeries {R : Type u} [CommRing R] (f : PowerSeries R) {m k : ℕ} (hkm : k ≤ m) : (ofPowerSeries f).truncate k hkm = ofPowerSeries f

Truncating an already truncated Mathlib series to a smaller precision is the direct truncation at that precision.

@[simp]

theorem HexTruncatedSeriesTheory.mulXPow_ofPowerSeries {R : Type u} {n : ℕ} [CommRing R] (f : PowerSeries R) (k : ℕ) : (ofPowerSeries f).mulXPow k = ofPowerSeries (PowerSeries.X ^ k * f)

Executable multiplication by x^k is truncation of multiplication by Mathlib's X^k.

theorem HexTruncatedSeriesTheory.coeff_deriv_ofPowerSeries {R : Type u} {n : ℕ} [CommRing R] (f : PowerSeries R) (i : ℕ) (hi : i < n - 1) : (ofPowerSeries f).deriv.coeff i = (PowerSeries.coeff i) (PowerSeries.derivative f)

Coefficients of a truncated derivative agree with Mathlib's formal derivative wherever both are represented.

@[simp]

theorem HexTruncatedSeriesTheory.deriv_ofPowerSeries {R : Type u} {n : ℕ} [CommRing R] (f : PowerSeries R) : (ofPowerSeries f).deriv = ofPowerSeries (PowerSeries.derivative f)

Executable differentiation commutes with truncation, at the precision lost by differentiation.