FreeProduct — Mathlib

English

The free product of the collection of R-algebras is defined as the quotient of FreeTensorAlgebra by the generating relation.

Русский

Свободное произведение коллекции R-алгебр определяется как частное от FreeTensorAlgebra по порождающему отношению.

LaTeX

$$$\\text{FreeProduct} := \\text{RingQuot} (FreeProduct.rel R A)$$$

Lean4

/-- The free product of the collection of `R`-algebras `A i`, as a quotient of
`FreeTensorAlgebra R A` -/
@[reducible]
def _root_.LinearAlgebra.FreeProduct :=
  RingQuot <| FreeProduct.rel R A

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