instNonUnitalCommRing — Mathlib

English

Let R be a nonunital commutative ring. Then the germ construction along a filter l assigns to R a nonunital commutative ring structure on Germ(l, R).

Русский

Пусть R — коммутативное кольцо без единицы. Тогда жермы вдоль фильтра l образуют кольцо без единицы.

LaTeX

$$$\\mathrm{NonUnitalCommRing}(\\mathrm{Germ}(l,R))$$$

Lean4

instance instNonUnitalCommRing [NonUnitalCommRing R] : NonUnitalCommRing (Germ l R)
    where
  __ := instNonUnitalRing
  __ := instCommSemigroup

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