algebraMap_eval_C — Mathlib

English

Algebra map preserves evaluation for C-polynomials.

Русский

Алгебраическое отображение сохраняет значение для C-полиномов.

LaTeX

$$$ algebraMap\ R\ R'\left((C_R\ n).eval\ x\right) = (C_R'\ n).eval\(algebraMap\ R\ R'\ x\right) $$$

Lean4

@[simp]
theorem algebraMap_eval_C [Algebra R R'] (x : R) (n : ℤ) :
    algebraMap R R' ((C R n).eval x) = (C R' n).eval (algebraMap R R' x) := by
  rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_C]

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