instRing — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- Product of two rings is a ring. -/
instance instRing [Ring R] [Ring S] : Ring (R × S) :=
  { inferInstanceAs (Semiring (R × S)), inferInstanceAs (AddCommGroup (R × S)),
    inferInstanceAs (AddGroupWithOne (R × S)) with }

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