module — Mathlib

English

There is a canonical map that forgets the σ-semi-linear structure, sending a σ₁₃-semi-linear map M →SL[σ₁₃] M₃ to a standard continuous linear map M →L[R] M₃.

Русский

Существует естественный переход от отображений типа σ₁₃-semi-линейных к обычным непрерывным линейным отображениям, забывающий структуру полулинейности.

LaTeX

$$$$ \text{coeLM} : (M \toSL[σ_{13}] M_3) \to L[R](M, M_3). $$$$

Lean4

instance module : Module S₃ (M →SL[σ₁₃] M₃)
    where
  zero_smul _ := ext fun _ => zero_smul S₃ _
  add_smul _ _ _ := ext fun _ => add_smul _ _ _

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