English
If M acts on α and N acts on α with Mᵐᵒᵖ acting on N and all centrality conditions hold, then IsScalarTower Mᵐᵒᵖ N α holds with smul_assoc: (unop m) • (n • a) = (m • n) • a.
Русский
Если M действует на α, и N действует на α, причём N действует через Mᵐᵒᵖ, и выполняются условия центральности, то IsScalarTower Mᵐᵒᵖ N α соблюдается со свойством smul_assoc: (unop m) • (n • a) = (m • n) • a.
LaTeX
$$$ \forall m \in M^{-1}, n \in N, a \in α,
(\mathrm{unop}(m)) \cdot (n \cdot a) = (m \cdot n) \cdot a. $$$
Lean4
@[to_additive]
instance (priority := 50) op_left [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] [SMul M N] [SMul Mᵐᵒᵖ N]
[IsCentralScalar M N] [SMul N α] [IsScalarTower M N α] : IsScalarTower Mᵐᵒᵖ N α where
smul_assoc m n a := by rw [← unop_smul_eq_smul m (n • a), ← unop_smul_eq_smul m n, smul_assoc]
