instDistrib — Mathlib

English

If R is distributive with ContinuousMul and ContinuousAdd, then SeparationQuotient R is Distrib.

Русский

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

LaTeX

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

Lean4

instance instDistrib [Distrib R] [ContinuousMul R] [ContinuousAdd R] : Distrib (SeparationQuotient R) :=
  surjective_mk.distrib mk mk_add mk_mul

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