instNonUnitalNonAssocCommSemiring

English

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

Русский

Если R — неединообразная коммутативная полугруппа без единицы с IsTopologicalSemiring, SeparationQuotient R — NonUnitalNonAssocCommSemiring.

LaTeX

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

Lean4

instance instNonUnitalNonAssocCommSemiring [NonUnitalNonAssocCommSemiring R] [IsTopologicalSemiring R] :
    NonUnitalNonAssocCommSemiring (SeparationQuotient R) :=
  surjective_mk.nonUnitalNonAssocCommSemiring mk mk_zero mk_add mk_mul mk_smul

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