toUnder_hom_right_apply — Mathlib

English

For a morphism f: A → B, the right component of f.toUnder.hom evaluated at a ∈ A is f(a).

Русский

Для гомоморфизма f: A → B правая компонента f.toUnder.hom на элементе a ∈ A равна f(a).

LaTeX

$$$f.toUnder.hom.right(a) = f(a)$$$

Lean4

@[simp]
theorem toUnder_hom_right_apply {A B : Type u} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B)
    (a : A) : f.toUnder.hom.right a = f a :=
  rfl

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