instNonAssocSemiring — Mathlib

English

If R is a NonUnitalNonAssocSemiring with IsTopologicalSemiring, SeparationQuotient R is a NonUnitalNonAssocSemiring.

Русский

Если R — NonUnitalNonAssocSemiring с IsTopologicalSemiring, SeparationQuotient R — NonUnitalNonAssocSemiring.

LaTeX

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

Lean4

instance instNonAssocSemiring [NonAssocSemiring R] [IsTopologicalSemiring R] :
    NonAssocSemiring (SeparationQuotient R) :=
  surjective_mk.nonAssocSemiring mk mk_zero mk_one mk_add mk_mul mk_smul mk_natCast

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