eval_map — Mathlib

English

For a linear map f, a polynomial q, and r ∈ R, eval r (map R f q) = f (eval r q).

Русский

Для линейного отображения f, полинома q и r ∈ R, eval r (map R f q) = f (eval r q).

LaTeX

$$$\\operatorname{eval} r (\\operatorname{map} R f q) = f \\big( \\operatorname{eval} r q \\big)$$$

Lean4

@[simp]
theorem eval_map (f : M →ₗ[R] M') (q : PolynomialModule R M) (r : R) :
    eval (algebraMap R R' r) (map R' f q) = f (eval r q) := by
  induction q using induction_linear with
  | zero => simp_rw [map_zero]
  | add f g e₁ e₂ => simp_rw [map_add, e₁, e₂]
  | single i m => simp only [map_single, eval_single, f.map_smul]; module

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