trunc_map — Mathlib

English

For a ring hom f, trunc n of the map of p equals the map of trunc n p.

Русский

Для гомоморфизма кольца f: trunc n (p.map f) = (trunc n p).map f.

LaTeX

$$$\\forall {R,S} [\\mathrm{Semiring}\, R] [\\mathrm{Semiring}\, S] (f : R \\to\\text{+}* S) (p : R⟦X⟧) (n : \\mathbb{N}),\\; \\operatorname{trunc} n (p.map f) = (\\operatorname{trunc} n p).map f$$$

Lean4

theorem trunc_map (p : R⟦X⟧) (n : ℕ) : (p.map f).trunc n = (p.trunc n).map f := by ext m;
  simp [coeff_trunc, apply_ite f]

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