instNonUnitalCommSemiring — Mathlib

English

Product of two NonUnitalCommSemirings is a NonUnitalCommSemiring.

Русский

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

LaTeX

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

Lean4

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

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