coe_aevalAeval_eq_evalEval — Mathlib

English

For x,y ∈ A, the underlying function of the two-variable evaluation morphism aevalAeval x y coincides with the standard evaluation map evalEval x y.

Русский

Для x,y ∈ A соответствие двухпеременной оценки совпадает с обычной оценкой evalEval x y как отображения.

LaTeX

$$$\\operatorname{coe}(\\mathrm{aevalAeval}(x,y)) = \\mathrm{evalEval}(x,y)$$$

Lean4

theorem coe_aevalAeval_eq_evalEval (x y : A) : ⇑(aevalAeval x y) = evalEval x y := by ext p;
  simp [aevalAeval, evalEval, aeval, Algebra.ofId]

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