Theorems · Theorem · linear algebra

CliffordAlgebra.odd_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) {P : (x : CliffordAlgebra Q) → x ∈ CliffordAlgebra.evenOdd Q 1 → Prop},
  (∀ (v : M), P ((CliffordAlgebra.ι Q) v) ⋯) →
    (∀ (x y : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q 1) (hy : y ∈ CliffordAlgebra.evenOdd Q 1),
        P x hx → P y hy → P (x + y) ⋯) →
      (∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q 1),
          P x hx → P ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x) ⋯) →
        ∀ (x : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q 1), P x hx

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

Defined in

Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule