ring — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance ring [∀ i, Ring <| f i] : Ring (∀ i : I, f i) :=
  { Pi.semiring, Pi.addCommGroup, Pi.addGroupWithOne with }

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