toRingHom_toAlgHom — Mathlib

English

For any F with FunLike, RingHomClass toRingHom (AlgHomClass.toAlgHom f) equals RingHomClass.toRingHom f.

Русский

Для любого F с FunLike, RingHomClass.toRingHom (AlgHomClass.toAlgHom f) равно RingHomClass.toRingHom f.

LaTeX

$$$$ \mathrm{toRingHom}(\mathrm{AlgHomClass.toAlgHom} f) = \mathrm{toRingHom} f. $$$$

Lean4

@[simp]
theorem toRingHom_toAlgHom {R A B : Type*} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B]
    {F : Type*} [FunLike F A B] [AlgHomClass F R A B] (f : F) :
    RingHomClass.toRingHom (AlgHomClass.toAlgHom f) = RingHomClass.toRingHom f :=
  rfl

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