instRing — Mathlib

English

If R is a commutative ring and each A_i is a ring with compatible algebra structures, then the PiTensorProduct has a canonical ring structure extending the semiring and abelian group structure.

Русский

Если R — коммутативное кольцо, а каждый A_i — кольцо с совместимыми алгебраическими структурами, то PiTensorProduct имеет каноническую кольцевую структуру, расширяющую полукольцо и абелеву группу.

LaTeX

$$$Ring(\\⨂[R] i, A i)$$$

Lean4

instance instRing : Ring (⨂[R] i, A i) where
  __ := instSemiring
  __ := inferInstanceAs <| AddCommGroup (⨂[R] i, A i)

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