mulAction — Mathlib

English

There is a left action of S2 on the space of continuous semilinear maps M1 →SL[σ12] M2 given by (a • f)(x) = a • f(x). This action satisfies 1 • f = f and (a b) • f = a • (b • f).

Русский

Существует левое действие множителя S2 на пространство непрерывных полулинейных отображений M1 →SL[σ12] M2, заданное формулой (a • f)(x) = a • f(x); выполняются тождества 1 • f = f и (a b) • f = a • (b • f).

LaTeX

$$$ 1 \cdot f = f, \quad (a b) \cdot f = a \cdot (b \cdot f). $$$

Lean4

instance mulAction : MulAction S₂ (M₁ →SL[σ₁₂] M₂)
    where
  one_smul _f := ext fun _x => one_smul _ _
  mul_smul _a _b _f := ext fun _x => mul_smul _ _ _

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