English
If M acts on α and Mᵐᵒᵖ acts with IsCentralScalar and M N actions commute, then SMulCommClass Mᵐᵒᵖ N α holds with the formula (unop m) • (n • a) = (nco) • (a).
Русский
Если M действует на α и Mᵐᵒᵖ действует с IsCentralScalar и действия M и N commute, то SMulCommClass Mᵐᵒᵖ N α выполняется.
LaTeX
$$$ \forall m \in M, n \in N, a \in α,
(\operatorname{unop} m) \cdot (n \cdot a) = n \cdot ( (\operatorname{unop} m) \cdot a ). $$$
Lean4
@[to_additive]
instance (priority := 50) op_left [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] [SMul N α] [SMulCommClass M N α] :
SMulCommClass Mᵐᵒᵖ N α :=
⟨fun m n a ↦ by rw [← unop_smul_eq_smul m (n • a), ← unop_smul_eq_smul m a, smul_comm]⟩
