instNonUnitalRing — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance instNonUnitalRing [NonUnitalRing R] [NonUnitalRing S] : NonUnitalRing (R × S) :=
  { inferInstanceAs (NonUnitalNonAssocRing (R × S)), inferInstanceAs (NonUnitalSemiring (R × S)) with }

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