trunc'_map — Mathlib

English

The trunc' map commutes with polynomial maps under RingHom, i.e., trunc' S n (map f p) = map f (trunc' R n p).

Русский

Усечение' коммутирует с отображениями по многочлену через RingHom: trunc' S n (map f p) = map f (trunc' R n p).

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]

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