toAlgHom — Mathlib

English

Every F with FunLike and AlgHomClass can be coerced to an actual AlgHom; this is the default coercion from F to A →ₐ[R] B.

Русский

У каждого F с FunLike и AlgHomClass есть преобразование к реальному AlgHom; это дефолтное преобразование из F в A →ₐ[R] B.

LaTeX

$$$F \\toAlgHom[R,A,B]\,\\inference$$$

Lean4

/-- Turn an element of a type `F` satisfying `AlgHomClass F α β` into an actual
`AlgHom`. This is declared as the default coercion from `F` to `α →+* β`. -/
@[coe]
def toAlgHom {F : Type*} [FunLike F A B] [AlgHomClass F R A B] (f : F) : A →ₐ[R] B
    where
  __ := (f : A →+* B)
  toFun := f
  commutes' := AlgHomClass.commutes f

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