instMonoidWithZero — Mathlib

English

If M₀ is a MonoidWithZero with continuous multiplication, then SeparationQuotient M₀ is a MonoidWithZero.

Русский

Если M₀ — моноид с нулём и единицей и умножение непрерывно, тогда SeparationQuotient M₀ образует MonoidWithZero.

LaTeX

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

Lean4

instance instMonoidWithZero [MonoidWithZero M₀] [ContinuousMul M₀] : MonoidWithZero (SeparationQuotient M₀) :=
  surjective_mk.monoidWithZero mk mk_zero mk_one mk_mul mk_pow

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