algebraMap_eval_S — Mathlib

English

Algebra map preserves evaluation for S-polynomials.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem algebraMap_eval_S [Algebra R R'] (x : R) (n : ℤ) :
    algebraMap R R' ((S R n).eval x) = (S R' n).eval (algebraMap R R' x) := by
  rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_S]

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