English
Let α and M be monoids with a distributive action of α on M, and IsScalarTower α M M. If c is a congruence on M, then the quotient c.Quotient carries a MulDistribMulAction of α, i.e., the action distributes over multiplication on the quotient.
Русский
Пусть α, M — моноиды, на M задано распределимое действие α на M, и выполняется IsScalarTower α M M. Тогда фактор-множество M/с наследует действие MulDistribMulAction от α: распределение действует на умножение в факторе.
LaTeX
$$$MulDistribMulAction\\ α\\ (c.Quotient)$$$
Lean4
instance mulDistribMulAction {α M : Type*} [Monoid α] [Monoid M] [MulDistribMulAction α M] [IsScalarTower α M M]
(c : Con M) : MulDistribMulAction α c.Quotient :=
{ smul_one := fun _ => congr_arg Quotient.mk'' <| smul_one _
smul_mul := fun _ => Quotient.ind₂' fun _ _ => congr_arg Quotient.mk'' <| smul_mul' _ _ _ }
