map_comp — Mathlib

English

For polynomials p, q: map f (p ∘ q) = (map f p) ∘ (map f q).

Русский

Для полиномов p, q: map f (p ∘ q) = (map f p) ∘ (map f q).

LaTeX

$$$$ \\operatorname{map} f (p.comp q) = (\\operatorname{map} f p).comp (\\operatorname{map} f q) $$$$

Lean4

theorem map_comp (p q : R[X]) : map f (p.comp q) = (map f p).comp (map f q) :=
  Polynomial.induction_on p (by simp only [map_C, forall_const, C_comp])
    (by simp +contextual only [Polynomial.map_add, add_comp, forall_const, imp_true_iff])
    (by
      simp +contextual only [pow_succ, ← mul_assoc, comp, forall_const, eval₂_mul_X, imp_true_iff, map_X,
        Polynomial.map_mul])

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