instMulZeroOneClass — Mathlib

English

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

Русский

Если M₀ имеет MulZeroOneClass и непрерывность умножения, то SeparationQuotient M₀ наследует MulZeroOneClass.

LaTeX

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

Lean4

instance instMulZeroOneClass [MulZeroOneClass M₀] [ContinuousMul M₀] : MulZeroOneClass (SeparationQuotient M₀) :=
  surjective_mk.mulZeroOneClass mk mk_zero mk_one mk_mul

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