semilinearMapClass — Mathlib

English

There is a FunLike structure for the type of σ-semi-linear maps M →ₛₗ[σ] M3, with the canonical coe toFun and a proof that equal semilinear maps agree in functions.

Русский

Для типа σ-семилинейных отображений M →ₛₗ[σ] M3 существует структура FunLike, с каноническим переходом к функции и доказательством того, что равные полулинейные отображения совпадают как функции.

LaTeX

$$$\mathrm{FunLike}\ (M \to_\sigma M_3)\ M\ M_3$$$

Lean4

instance semilinearMapClass : SemilinearMapClass (M →ₛₗ[σ] M₃) σ M M₃
    where
  map_add f := f.map_add'
  map_smulₛₗ := LinearMap.map_smul'

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