instSMulCommClass — Mathlib

English

If S and T act on the quaternion algebra, these actions commute: s · t · x = t · s · x for all s ∈ S, t ∈ T, x ∈ ℍ.

Русский

Если S и T действуют на алгебру кватернионов, эти действия коммутируют: s · t · x = t · s · x.

LaTeX

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

Lean4

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

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