instIsScalarTower — Mathlib

English

If S,T act on R with IsScalarTower, then S,T act on QuadraticAlgebra R a b with the same tower: smul_assoc holds.

Русский

Если S и T действуют на R с учетом IsScalarTower, то они действуют на QuadraticAlgebra R a b с тем же тензорным трюком: ассоциативность умножения выполняется.

LaTeX

$$$\\forall s:\\, S, t:\\, T, z:\\, QuadraticAlgebra R a b,\\ smul\\_assoc\; s\\; t\\; z:\\; (s t)\\! z = s\\! (t\\! z).$$$

Lean4

instance [SMul S T] [IsScalarTower S T R] : IsScalarTower S T (QuadraticAlgebra R a b) where
  smul_assoc s t z := by ext <;> exact smul_assoc _ _ _

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