instFunLike_1 — Mathlib

English

There is a canonical FunLike instance on the type of nonunital algebra homomorphisms, providing a uniform way to regard these objects as functions with extra structure.

Русский

Существует канонический экземпляр FunLike для типа гомоморфизмов алгебры без единицы, задающий единый способ рассматривать эти объекты как функции с дополнительной структурой.

LaTeX

$$$\text{There exists }\mathrm{FunLike}(A \to_{\varphi} B)\, A\, B$$$

Lean4

instance : FunLike (A →ₛₙₐ[φ] B) A B where
  coe f := f.toFun
  coe_injective' := coe_injective

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