instFunLike — Mathlib

English

An instance of FunLike for QuadraticMap provides a coherent way to treat quadratic maps as functions that can be coerced to functions M → N.

Русский

Экземпляр FunLike для QuadraticMap обеспечивает единый способ трактовки квадратичных отображений как функций M → N и их приведений к функциям.

LaTeX

$$$$ \\text{QuadraticMap} \\; R \\; M \\; N \\; \\text{is an instance of } FunLike(M,N). $$$$

Lean4

instance instFunLike : FunLike (QuadraticMap R M N) M N
    where
  coe := toFun
  coe_injective' x y h := by cases x; cases y; congr

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