instSMulCommClass — Mathlib

English

Another IsScalarTower relation between S, T and 𝓜(𝕜,A) ensuring compatibility of two scalar actions with the multiplier structure.

Русский

Другая связь IsScalarTower между S, T и 𝓜(𝕜,A), обеспечивающая совместимость двух скалярных действий с структурой умножителей.

LaTeX

$$$$ \\text{IsScalarTower}(S,T, 𝓜(𝕜,A)) $$$$

Lean4

instance instSMulCommClass [SMulCommClass S T A] : SMulCommClass S T 𝓜(𝕜, A) where
  smul_comm _ _ a := ext (𝕜 := 𝕜) (A := A) _ _ <| smul_comm _ _ a.toProd

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