instRightDistribClass — Mathlib

English

If R has RightDistribClass with ContinuousMul, then SeparationQuotient R inherits RightDistribClass.

Русский

Если R обладает правым распределением и непрерывным умножением, SeparationQuotient R наследует правое распределение.

LaTeX

$$$RightDistribClass\left(\mathrm{SeparationQuotient}(R)\right)$$$

Lean4

instance instRightDistribClass [Mul R] [Add R] [RightDistribClass R] [ContinuousMul R] [ContinuousAdd R] :
    RightDistribClass (SeparationQuotient R) :=
  surjective_mk.rightDistribClass mk mk_add mk_mul

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