instSemigroupWithZero — Mathlib

English

If M₀ is a semigroup with zero and multiplication is continuous, then the separation quotient of M₀ is a SemigroupWithZero.

Русский

Если M₀ — полугруппа с нулём и умножение непрерывно, разделительная фактор-группа M₀ образует SemigroupWithZero.

LaTeX

$$$SemigroupWithZero\left(\mathrm{SeparationQuotient}(M_0)\right)$$$

Lean4

instance instSemigroupWithZero [SemigroupWithZero M₀] [ContinuousMul M₀] : SemigroupWithZero (SeparationQuotient M₀) :=
  surjective_mk.semigroupWithZero mk mk_zero mk_mul

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