instCommSemiring — Mathlib

English

Product of two commutative semirings is a commutative semiring.

Русский

Произведение двух коммутативных полукольц является коммутативным полукольцом.

LaTeX

$$$\text{CommSemiring}(R \times S)$$$

Lean4

/-- Product of two commutative semirings is a commutative semiring. -/
instance instCommSemiring [CommSemiring R] [CommSemiring S] : CommSemiring (R × S) :=
  { inferInstanceAs (Semiring (R × S)), inferInstanceAs (CommMonoid (R × S)) with }

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