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