instCommRing — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- Product of two commutative rings is a commutative ring. -/
instance instCommRing [CommRing R] [CommRing S] : CommRing (R × S) :=
  { inferInstanceAs (Ring (R × S)), inferInstanceAs (CommMonoid (R × S)) with }

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