English
For any α, β, M with a MulOneClass and compatible scalar actions and IsScalarTower, the quotient c.Quotient inherits a SMulCommClass structure, i.e., the actions of α and β commute on the quotient.
Русский
Для любых α, β, M с MulOneClass и совместимыми скалярами и IsScalarTower, тождество q выполняется на фактор-модуле: действия α и β коммутируют на c.Quotient.
LaTeX
$$SMulCommClass α β c.Quotient$$
Lean4
/-- The congruence relation on a monoid `M` from a submonoid of `M × M` for which membership
is an equivalence relation. -/
@[to_additive /-- The additive congruence relation on an `AddMonoid` `M` from
an `AddSubmonoid` of `M × M` for which membership is an equivalence relation. -/
]
def ofSubmonoid (N : Submonoid (M × M)) (H : Equivalence fun x y => (x, y) ∈ N) : Con M
where
r x y := (x, y) ∈ N
iseqv := H
mul' := N.mul_mem
