instMulZeroClass — Mathlib

English

If M₀ has a multiplicative structure with zero and multiplication is continuous, then the separation quotient of M₀ inherits a MulZeroClass structure.

Русский

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

LaTeX

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

Lean4

instance instMulZeroClass [MulZeroClass M₀] [ContinuousMul M₀] : MulZeroClass (SeparationQuotient M₀) :=
  surjective_mk.mulZeroClass mk mk_zero mk_mul

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