instCommSemigroup — Mathlib

English

If M is a commutative semigroup with continuous multiplication, then the separation quotient of M is a commutative semigroup under the induced operation.

Русский

Если M является коммутативной полугруппой с непрерывным умножением, то SeparationQuotient(M) является коммутативной полугруппой с индуцированной операцией.

LaTeX

$$$\operatorname{CommSemigroup}(\mathrm{SeparationQuotient}(M))$$$

Lean4

@[to_additive]
instance instCommSemigroup [CommSemigroup M] [ContinuousMul M] : CommSemigroup (SeparationQuotient M) :=
  surjective_mk.commSemigroup mk mk_mul

Похожие утверждения