algebraMap_eval_U — Mathlib

English

Analogous statement for U-polynomials under algebra maps.

Русский

Аналогичное утверждение для U-полиномов при алгебрационных отображениях.

LaTeX

$$$ algebraMap\ R\ R'\left((U_R\ n).eval\ x\right) = (U_{R'}\ n).eval\(algebraMap\ R\ R'\ x\right) $$$

Lean4

@[simp]
theorem algebraMap_eval_U [Algebra R R'] (x : R) (n : ℤ) :
    algebraMap R R' ((U R n).eval x) = (U R' n).eval (algebraMap R R' x) := by
  rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_U]

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