aeval_algHom — Mathlib

English

For any algebra homomorphism f : A →ₐ[R] B and x ∈ A, aeval (f(x)) = f ∘ aeval(x).

Русский

Для любого алгебра-гомоморфизма f: A →ₐ[R] B и элемента x ∈ A выполняется равенство aeval(f(x)) = f ∘ aeval(x).

LaTeX

$$$\forall f: A \to_{R} B,\; x\in A:\; \operatorname{aeval}(f(x)) = f \circ \operatorname{aeval}(x).$$$

Lean4

theorem aeval_algHom (f : A →ₐ[R] B) (x : A) : aeval (f x) = f.comp (aeval x) :=
  algHom_ext <| by simp only [aeval_X, AlgHom.comp_apply]

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