trunc_map — Mathlib

English

Truncation commutes with polynomial map: applying a ring homomorphism after truncation equals truncating after applying the map.

Русский

Усечение коммутирует с полиномиальным отображением: применение отображения после усечения эквивалентно усечению после применения отображения.

LaTeX

$$$$ \\operatorname{trunc} S n (\\operatorname{map} f p) = \\operatorname{map} f (\\operatorname{trunc} R n p). $$$$

Lean4

@[simp]
theorem trunc_map [CommSemiring S] (n : σ →₀ ℕ) (f : R →+* S) (p : MvPowerSeries σ R) :
    trunc S n (map f p) = MvPolynomial.map f (trunc R n p) := by ext m;
  simp [coeff_trunc, MvPolynomial.coeff_map, apply_ite f]

Похожие утверждения