theorem HexTruncatedSeriesTheory.natCast_succ {R : Type u} {n : ℕ} [CommRing R] (k : ℕ) : ↑(k + 1) = ↑k + 1

The core natural cast obeys Mathlib's successor law.

theorem HexTruncatedSeriesTheory.nsmul_zero {R : Type u} {n : ℕ} [CommRing R] (a : Hex.TSeries R n) : 0 • a = 0

The core natural scalar action obeys Mathlib's zero law.

theorem HexTruncatedSeriesTheory.nsmul_succ {R : Type u} {n : ℕ} [CommRing R] (k : ℕ) (a : Hex.TSeries R n) : (k + 1) • a = k • a + a

The core natural scalar action obeys Mathlib's successor law.

@[instance_reducible]

instance HexTruncatedSeriesTheory.commRing {R : Type u} {n : ℕ} [CommRing R] : CommRing (Hex.TSeries R n)

Mathlib's commutative-ring structure on truncated series, pinned to the executable operations from the Mathlib-free core.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HexTruncatedSeriesTheory.ofPowerSeries {R : Type u} {n : ℕ} [CommRing R] (f : PowerSeries R) : Hex.TSeries R n

Truncate a Mathlib power series to the first n coefficients.

Equations

• HexTruncatedSeriesTheory.ofPowerSeries f = Hex.TSeries.ofFn fun (i : ℕ) => (PowerSeries.coeff i) f

@[simp]

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

Coefficients of a truncated Mathlib power series agree below the precision.

noncomputable def HexTruncatedSeriesTheory.ofPowerSeriesHom {R : Type u} {n : ℕ} [CommRing R] : PowerSeries R →+* Hex.TSeries R n

Truncation from power series is a ring homomorphism.

Equations

• HexTruncatedSeriesTheory.ofPowerSeriesHom = { toFun := HexTruncatedSeriesTheory.ofPowerSeries, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

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

Applying the truncation ring homomorphism is definitionally the same as truncating a Mathlib power series.

theorem HexTruncatedSeriesTheory.ofPowerSeriesHom_surjective {R : Type u} {n : ℕ} [CommRing R] : Function.Surjective ⇑ofPowerSeriesHom

Every truncated series is represented by a Mathlib power series.

theorem HexTruncatedSeriesTheory.ker_ofPowerSeriesHom {R : Type u} {n : ℕ} [CommRing R] : RingHom.ker ofPowerSeriesHom = Ideal.span {PowerSeries.X ^ n}

The kernel of coefficient truncation is the principal ideal (X^n).

noncomputable def HexTruncatedSeriesTheory.quotEquiv {R : Type u} {n : ℕ} [CommRing R] : PowerSeries R ⧸ Ideal.span {PowerSeries.X ^ n} ≃+* Hex.TSeries R n

Fixed-precision series are power series modulo X^n.

Equations

• HexTruncatedSeriesTheory.quotEquiv = (Ideal.quotEquivOfEq ⋯).trans (RingHom.quotientKerEquivOfSurjective ⋯)

@[simp]

theorem HexTruncatedSeriesTheory.quotEquiv_mk {R : Type u} {n : ℕ} [CommRing R] (f : PowerSeries R) : quotEquiv ((Ideal.Quotient.mk (Ideal.span {PowerSeries.X ^ n})) f) = ofPowerSeries f

The quotient equivalence sends a power-series representative to its coefficient truncation.

@[instance_reducible, instance 800]

instance HexTruncatedSeriesTheory.natInversesOfAlgebra {R : Type u} [CommRing R] [Algebra ℚ R] (m : ℕ) : Hex.TSeries.NatInverses R m

A rational algebra contains every natural inverse required by the Mathlib-free algorithms.

Equations

• HexTruncatedSeriesTheory.natInversesOfAlgebra m = { invNat := fun (k : ℕ) => if k = 0 then 0 else (algebraMap ℚ R) (↑k)⁻¹, invNat_eq := ⋯ }