instSemilinearMapClass — Mathlib

English

There is a semilinear map class structure for DistribMulActionHom, giving semilinear maps from M to M2 with σ.

Русский

Существует структура класса семилинейных отображений для DistribMulActionHom, задающая семилинейные отображения из M в M2 с параметром σ.

LaTeX

$$$\text{SemilinearMapClass } (DistribMulActionHom \; σ) M M_2$$$

Lean4

instance : SemilinearMapClass (M →ₑ+[σ.toMonoidHom] M₂) σ M M₂ where

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