English
A symmetric induction principle for the odd part, mirroring the even-induction with vectors as generators.
Русский
Симметричная индукция по нечётной части, аналогичная по структуре индукции по чётной части с векторами как генераторами.
LaTeX
$$odd_induction(Q, P, ι, add, ι_mul_ι_mul, x, hx)$$
Lean4
/-- 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. -/
@[elab_as_elim]
theorem odd_induction {P : ∀ x, x ∈ evenOdd Q 1 → Prop} (ι : ∀ v, P (ι Q v) (ι_mem_evenOdd_one _ _))
(add : ∀ x y hx hy, P x hx → P y hy → P (x + y) (Submodule.add_mem _ hx hy))
(ι_mul_ι_mul :
∀ m₁ m₂ x hx,
P x hx →
P (CliffordAlgebra.ι Q m₁ * CliffordAlgebra.ι Q m₂ * x)
(zero_add (1 : ZMod 2) ▸ SetLike.mul_mem_graded (ι_mul_ι_mem_evenOdd_zero Q m₁ m₂) hx))
(x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1) : P x hx :=
by
refine evenOdd_induction _ _ (motive := P) (fun ιv => ?_) add ι_mul_ι_mul x hx
simp_rw [ZMod.val_one, pow_one]
rintro ⟨v, rfl⟩
exact ι v
