Theorems · Definition · ring theory

LinearAlgebra.FreeProduct.ringCon

{I : Type u} →
  [DecidableEq I] →
    (R : Type v) →
      [inst : CommSemiring R] →
        (A : I → Type w) →
          [inst_1 : (i : I) → Semiring (A i)] →
            [inst_2 : (i : I) → Algebra R (A i)] → RingCon (LinearAlgebra.FreeProduct.FreeTensorAlgebra R A)

rel as a ring congruence.

Defined in

Mathlib.LinearAlgebra.FreeProduct.Basic

Cited by

8 results in Mathlib

Foundations

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

Assumes

DecidableEqCommSemiringSemiringAlgebra