ofHom_apply — Mathlib

English

For any algebra hom f: X →ₐ[R] Y and any x ∈ X, the underlying function of the corresponding AlgCat morphism is given by applying f to x: ofHom f x = f x.

Русский

Для любого гомоморфизма алгебр f: X →ₐ[R] Y и любого элемента x ∈ X соответствующий морфизм AlgCat действует так: ofHom f x = f x.

LaTeX

$$$\\operatorname{ofHom} f\\, x = f\\, x$$$

Lean4

theorem ofHom_apply {R : Type u} [CommRing R] {X Y : Type v} [Ring X] [Algebra R X] [Ring Y] [Algebra R Y]
    (f : X →ₐ[R] Y) (x : X) : ofHom f x = f x :=
  rfl

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