English
Let α act on the quotient RingCon R, and assume the action is compatible with ring operations. Then the induced action on c.Quotient forms a scalar tower, i.e., for all a ∈ α and x, y ∈ c.Quotient, (a · x) · y = a · (x · y).
Русский
Пусть α действует на фактор RingCon R, и это действие совместимо с операциями кольца. Тогда индуцированное действие на c.Quotient образует скаляровый торов, т.е. для всех a ∈ α и x, y ∈ c.Quotient выполняется (a · x) · y = a · (x · y).
LaTeX
$$$$ (a \cdot x) \cdot y = a \cdot (x \cdot y) $$$$
Lean4
instance isScalarTower_right [Add R] [MulOneClass R] [SMul α R] [IsScalarTower α R R] (c : RingCon R) :
IsScalarTower α c.Quotient c.Quotient where
smul_assoc _ := Quotient.ind₂' fun _ _ => congr_arg Quotient.mk'' <| smul_mul_assoc _ _ _
