instFunLike — Mathlib

English

A convenient FunLike structure is provided for AlgEquiv, identifying the action of AlgEquiv elements as functions.

Русский

Для AlgEquiv задана удобная структура FunLike, фиксирующая действие элементов AlgEquiv как функций.

LaTeX

$$FunLike (AlgEquiv R A B) A B$$

Lean4

/-- Helper instance since the coercion is not always found. -/
instance : FunLike (A₁ ≃ₐ[R] A₂) A₁ A₂ where
  coe := DFunLike.coe
  coe_injective' := DFunLike.coe_injective'

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