instSemiring — Mathlib

English

If R'–R algebra structures and A_i are algebras in their own right, then the PiTensorProduct acquires a canonical algebra structure over R'.

Русский

Если заданы алгебраические структуры R'–R и A_i сами по себе являются алгебрами, PiTensorProduct получает каноническую алгебраическую структуру над R'.

LaTeX

$$$Algebra\\ R'\\ (\\bigotimes_R i, A_i)$$$

Lean4

instance instSemiring : Semiring (⨂[R] i, A i)
    where
  __ := instNonUnitalSemiring
  __ := instNonAssocSemiring

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