English
Let α be a monoid acting on M by a MulAction, and let c be a congruence on M. If the action is compatible with the congruence (IsScalarTower α M M), then α induces a well-defined action on the quotient M / c by defining a · [m] = [a · m]. This induced action satisfies the axioms of a MulAction: 1 · [m] = [m] and (ab) · [m] = a · (b · [m]).
Русский
Пусть α — моноид, действующий на множество M следующими свойствами, и c — конгруэнция на M. Если действие совместимо с конгруэнцией (условие IsScalarTower α M M), то α индуцирует корректное действие на фактор-множество M / c, задаваемое: a · [m] = [a · m]. Это действие удовлетворяет аксиомам действия моноида: 1 · [m] = [m] и (ab) · [m] = a · (b · [m]).
LaTeX
$$$MulAction\\ α\\ (c.Quotient)$$$
Lean4
@[to_additive]
instance mulAction {α M : Type*} [Monoid α] [MulOneClass M] [MulAction α M] [IsScalarTower α M M] (c : Con M) :
MulAction α c.Quotient
where
one_smul := Quotient.ind' fun _ => congr_arg Quotient.mk'' <| one_smul _ _
mul_smul _ _ := Quotient.ind' fun _ => congr_arg Quotient.mk'' <| mul_smul _ _ _
