instNonUnitalCommRing — Mathlib

English

If R and S are nonunital commutative rings, then R × S is a nonunital commutative ring.

Русский

Если R и S — неполные коммутативные кольца без единицы, то R × S является коммутативным кольцом без единицы.

LaTeX

$$$[ \\text{NonUnitalCommRing }R] \\; [\\text{NonUnitalCommRing }S] \\Rightarrow\\; \\text{NonUnitalCommRing }(R \\times S).$$$

Lean4

/-- Product of two `NonUnitalCommRing`s is a `NonUnitalCommRing`. -/
instance instNonUnitalCommRing [NonUnitalCommRing R] [NonUnitalCommRing S] : NonUnitalCommRing (R × S) :=
  { inferInstanceAs (NonUnitalRing (R × S)), inferInstanceAs (CommSemigroup (R × S)) with }

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