instHasDistribNeg — Mathlib

English

Let R be a topological ring with a distributive negation and continuous multiplication and negation. Then the separation quotient SeperationQuotient(R) inherits a distributive negation, i.e. HasDistribNeg (SeparationQuotient R).

Русский

Пусть R — топологическое кольцо с распределённым отрицанием, непрерывным умножением и непрерывностью отрицания. Тогда разделительная квота SeparationQuotient(R) наследует распределённое отрицание: HasDistribNeg(SeparationQuotient R).

LaTeX

$$$\text{HasDistribNeg}(\mathrm{SeparationQuotient}\,R)$$$

Lean4

instance instHasDistribNeg [Mul R] [HasDistribNeg R] [ContinuousMul R] [ContinuousNeg R] :
    HasDistribNeg (SeparationQuotient R) :=
  surjective_mk.hasDistribNeg mk mk_neg mk_mul

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