instNonUnitalSemiring — Mathlib

English

Product of two NonUnitalSemirings is a NonUnitalSemiring.

Русский

Произведение двух NonUnitalSemiring образует NonUnitalSemiring.

LaTeX

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

Lean4

/-- Product of two `NonUnitalSemiring`s is a `NonUnitalSemiring`. -/
instance instNonUnitalSemiring [NonUnitalSemiring R] [NonUnitalSemiring S] : NonUnitalSemiring (R × S) :=
  { inferInstanceAs (NonUnitalNonAssocSemiring (R × S)), inferInstanceAs (SemigroupWithZero (R × S)) with }

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