Theorems · Theorem · ring theory

CliffordAlgebra.induction

∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {C : CliffordAlgebra Q → Prop},
  (∀ (r : R), C ((algebraMap R (CliffordAlgebra Q)) r)) →
    (∀ (x : M), C ((CliffordAlgebra.ι Q) x)) →
      (∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)) →
        (∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)) → ∀ (a : CliffordAlgebra Q), C a

If C holds for the algebraMap of r : R into CliffordAlgebra Q, the ι of x : M, and is preserved under addition and multiplication, then it holds for all of CliffordAlgebra Q. See also the stronger CliffordAlgebra.left_induction and CliffordAlgebra.right_induction.

Defined in

Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Cited by

8 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule