coe_aeval — Mathlib

English

Same as above: the coercion of aeval equals eval₂ with algebra map.

Русский

То же самое: приведение k aeval совпадает с eval₂ через алгебраическое отображение.

LaTeX

$$$$\uparrow(\operatorname{aeval}(ha)) = \operatorname{eval}_{\text{algebraMap}(R,S)}^{a}.$$$$

Lean4

theorem coe_aeval (ha : HasEval a) : ↑(aeval ha) = eval₂ (algebraMap R S) a := by
  simp only [aeval, AlgHom.coe_mk, coe_eval₂Hom]

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