aeval_algEquiv — Mathlib

English

For any algebra equivalence f: A ≃ₐ[R] B, aeval(f(x)) = (f).comp (aeval x).

Русский

Для алгебраического эквивалентности f: A ≃ₐ[R] B выполняется aeval(f(x)) = f ∘ aeval(x).

LaTeX

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

Lean4

theorem aeval_algEquiv (f : A ≃ₐ[R] B) (x : A) : aeval (f x) = (f : A →ₐ[R] B).comp (aeval x) :=
  aeval_algHom (f : A →ₐ[R] B) x

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