instIsScalarTower — Mathlib

English

There is a compatible scalar action of S and T on the quaternion algebra, i.e., the associativity of scalar actions holds: (s · t) · x = s · (t · x) for all s ∈ S, t ∈ T, x ∈ ℍ[R,c1,c2,c3].

Русский

Существует согласованное действие скаляров S и T на алгебре кватернионов: (s · t) · x = s · (t · x) для всех s ∈ S, t ∈ T, x ∈ ℍ.

LaTeX

$$$ (s \cdot t) \cdot x = s \cdot (t \cdot x)$$$

Lean4

instance [SMul S T] [IsScalarTower S T R] : IsScalarTower S T ℍ[R,c₁,c₂,c₃] where
  smul_assoc s t x := by ext <;> exact smul_assoc _ _ _

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