instCommRing — Mathlib

English

If R is a commutative ring with a topological ring structure, then the separation quotient is a commutative ring with unity.

Русский

Если R — коммутативное кольцо с топологической структурой кольца, то разделительная квота является коммутативным кольцом с единицей.

LaTeX

$$$\mathrm{CommRing}(\mathrm{SeparationQuotient}\,R)$$$

Lean4

instance instCommRing [CommRing R] [IsTopologicalRing R] : CommRing (SeparationQuotient R) :=
  surjective_mk.commRing mk mk_zero mk_one mk_add mk_mul mk_neg mk_sub mk_smul mk_smul mk_pow mk_natCast mk_intCast

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