instNonAssocSemiring — Mathlib

English

Product of two NonAssocSemirings is a NonAssocSemiring.

Русский

Произведение двух NonAssocSemiring является NonAssocSemiring.

LaTeX

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

Lean4

/-- Product of two `NonAssocSemiring`s is a `NonAssocSemiring`. -/
instance instNonAssocSemiring [NonAssocSemiring R] [NonAssocSemiring S] : NonAssocSemiring (R × S) :=
  { inferInstanceAs (NonUnitalNonAssocSemiring (R × S)), inferInstanceAs (MulZeroOneClass (R × S)),
    inferInstanceAs (AddMonoidWithOne (R × S)) with }

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