Theorems · Theorem · linear algebra

CliffordAlgebra.even_induction

∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) {motive : (x : CliffordAlgebra Q) → x ∈ CliffordAlgebra.evenOdd Q 0 → Prop},
  (∀ (r : R), motive ((algebraMap R (CliffordAlgebra Q)) r) ⋯) →
    (∀ (x y : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q 0) (hy : y ∈ CliffordAlgebra.evenOdd Q 0),
        motive x hx → motive y hy → motive (x + y) ⋯) →
      (∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q 0),
          motive x hx → motive ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x) ⋯) →
        ∀ (x : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q 0), motive x hx

To show a property is true on the even parts, it suffices to show it is true on the scalars, closed under addition, and under left-multiplication by a pair of vectors.

Defined in

Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule