coeTC — Mathlib

English

There is a canonical CoeTC instance from F to AlgHom R A B, allowing F to be treated as a function that returns algebra Hom's.

Русский

Существует канонический экземпляр CoeTC от F к AlgHom R A B, позволяющий трактовать F как отображение в алгебраические гомоморфизмы.

LaTeX

$$$F \\Rightarrow_{\\mathrm{AlgHom}} (R,A,B)$$$

Lean4

instance coeTC {F : Type*} [FunLike F A B] [AlgHomClass F R A B] : CoeTC F (A →ₐ[R] B) :=
  ⟨AlgHomClass.toAlgHom⟩

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