Theorems · Definition · ring theory

CliffordAlgebra.ringCon

{R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → QuadraticForm R M → RingCon (TensorAlgebra R M)

Rel as a ring congruence, used to build the quotient.

Defined in

Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule