Theorems · Definition · ring theory

LinearAlgebra.FreeProduct

{I : Type u} →
  [DecidableEq I] →
    (R : Type v) →
      [inst : CommSemiring R] →
        (A : I → Type w) → [inst_1 : (i : I) → Semiring (A i)] → [(i : I) → Algebra R (A i)] → Type (max (max u v) w)

The free product of the collection of R-algebras A i, as a quotient of FreeTensorAlgebra R A

Defined in

Mathlib.LinearAlgebra.FreeProduct.Basic

Cited by

11 results in Mathlib

Foundations

Depth 40 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqCommSemiringSemiringAlgebra