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