instMulOneClass — Mathlib

English

If M has a MulOneClass structure and continuous multiplication, then the SeparationQuotient M inherits a MulOneClass structure.

Русский

Если у M есть структура MulOneClass и непрерывное умножение, то SeparationQuotient(M) наследует MulOneClass.

LaTeX

$$$\operatorname{MulOneClass}(\mathrm{SeparationQuotient}(M))$$$

Lean4

@[to_additive]
instance instMulOneClass [MulOneClass M] [ContinuousMul M] : MulOneClass (SeparationQuotient M) :=
  surjective_mk.mulOneClass mk mk_one mk_mul

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