instSMulCommClass — Mathlib

English

If S and T act on N with commuting actions, then QuadraticMap carries a SMulCommClass structure; for all s in S, t in T, and Q in QuadraticMap, s • (t • Q) = t • (s • Q).

Русский

Если S и T действуют на N коммутирующими действиями, то множество квадратичных отображений получает структуру SMulCommClass: для любых s∈S, t∈T и Q∈QuadraticMap выполняется s·(t·Q) = t·(s·Q).

LaTeX

$$$\\forall s\\in S, \\forall t\\in T, \\forall Q\\in \\mathrm{QuadraticMap}(R,M,N),\\ s\\cdot (t\\cdot Q) = t\\cdot (s\\cdot Q).$$$

Lean4

instance [SMulCommClass S T N] : SMulCommClass S T (QuadraticMap R M N) where
  smul_comm _s _t _q := ext fun _ => smul_comm _ _ _

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