instCommRing — Mathlib

English

The tensor product ⨂[R] i, A_i, where each A_i is a commutative ring and an R-algebra, carries a natural commutative ring structure; i.e., the tensor product of a family of commutative rings is a commutative ring.

Русский

Тензорное произведение семейства коммутативных колец над R имеет естественную структуру коммутативного кольца.

LaTeX

$$⊗[R] i, A_i ∈ CommRing$$

Lean4

instance instCommRing : CommRing (⨂[R] i, A i)
    where
  __ := instCommSemiring
  __ := inferInstanceAs <| AddCommGroup (⨂[R] i, A i)

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