semiring — Mathlib

English

If every f(i) is a Semiring, then the function space ∀ i, f(i) is a Semiring with coordinatewise operations.

Русский

Если для каждого i совокупность f(i) образует полукольцо, то пространство функций, состоящее из функций i → f(i), образует полукольцо с покоординатными операциями.

LaTeX

$$$\forall i,\ Semiring(f(i)) \Rightarrow Semiring(\forall i: I, f(i))$$$

Lean4

instance semiring [∀ i, Semiring <| f i] : Semiring (∀ i : I, f i) :=
  { Pi.nonUnitalSemiring, Pi.nonAssocSemiring, Pi.monoidWithZero with }

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