instCommMagma — Mathlib

English

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

Русский

Если M имеет коммутативную магму и непрерывное умножение, то SeparationQuotient(M) образует коммутативную магму с использованием инференцированной операции.

LaTeX

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

Lean4

@[to_additive]
instance instCommMagma [CommMagma M] [ContinuousMul M] : CommMagma (SeparationQuotient M) :=
  surjective_mk.commMagma mk mk_mul

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