instCommMonoidWithZero — Mathlib

English

If M₀ is CommMonoidWithZero with ContinuousMul, then SeparationQuotient M₀ is CommMonoidWithZero.

Русский

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

LaTeX

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

Lean4

instance instCommMonoidWithZero [CommMonoidWithZero M₀] [ContinuousMul M₀] :
    CommMonoidWithZero (SeparationQuotient M₀) :=
  surjective_mk.commMonoidWithZero mk mk_zero mk_one mk_mul mk_pow

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