English
A specialized induction for the even part of the Clifford algebra using algebra maps and sums of generators.
Русский
Специализированная индукция по чётной части клиффордовой алгебры через алгебраические отображения и суммы генераторов.
LaTeX
$$even_induction(Q, motive, algebraMap, add, ι_mul_ι_mul, x, hx) $$
Lean4
/-- 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. -/
@[elab_as_elim]
theorem even_induction {motive : ∀ x, x ∈ evenOdd Q 0 → Prop}
(algebraMap : ∀ r : R, motive (algebraMap _ _ r) (SetLike.algebraMap_mem_graded _ _))
(add : ∀ x y hx hy, motive x hx → motive y hy → motive (x + y) (Submodule.add_mem _ hx hy))
(ι_mul_ι_mul :
∀ m₁ m₂ x hx,
motive x hx →
motive (ι Q m₁ * ι Q m₂ * x)
(zero_add (0 : ZMod 2) ▸ SetLike.mul_mem_graded (ι_mul_ι_mem_evenOdd_zero Q m₁ m₂) hx))
(x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 0) : motive x hx :=
by
refine evenOdd_induction _ _ (motive := motive) (fun rx h => ?_) add ι_mul_ι_mul x hx
obtain ⟨r, rfl⟩ := Submodule.mem_one.mp h
exact algebraMap r
