English
The induced quotient carries a commuting action of α and the quotient elements; i.e., the scalar action commutes with the ring operation on c.Quotient: a · x = x · a for all a ∈ α and x ∈ c.Quotient.
Русский
Индуцированное деление действует на c.Quotient так, что скалярное действие и элементы кварты коммутируют: a · x = x · a для всех a ∈ α и x ∈ c.Quotient.
LaTeX
$$$$ a \cdot x = x \cdot a \quad \text{for all } a \in \alpha, x \in c^{\Quotient} $$$$
Lean4
instance smulCommClass [Add R] [MulOneClass R] [SMul α R] [IsScalarTower α R R] [SMulCommClass α R R] (c : RingCon R) :
SMulCommClass α c.Quotient c.Quotient where
smul_comm _ := Quotient.ind₂' fun _ _ => congr_arg Quotient.mk'' <| (mul_smul_comm _ _ _).symm
