English
Let S and T act on N with IsScalarTower S T N and QuadraticMap R M N is defined; then the induced action on QuadraticMap R M N satisfies the scalar-tower associativity: s · (t · Q) = (s t) · Q for all s ∈ S, t ∈ T, Q ∈ QuadraticMap R M N.
Русский
Пусть S и T действуют на N и существует цепь скаляров IsScalarTower S T N; тогда на множестве квадратичных отображений QuadraticMap R M N задаётся совместное действие скаляров так, что ассоциативность выполняется: для всех s∈S, t∈T и Q∈QuadraticMap R M N имеет место s · (t · Q) = (s t) · Q.
LaTeX
$$$\\forall s \\in S, \\forall t \\in T, \\forall Q \\in \\text{QuadraticMap}(R,M,N):\\ s \\cdot (t \\cdot Q) = (s t) \\cdot Q.$$$
Lean4
instance [SMul S T] [IsScalarTower S T N] : IsScalarTower S T (QuadraticMap R M N) where
smul_assoc _s _t _q := ext fun _ => smul_assoc _ _ _
