English
For generator m ∈ M, folding over ι_Q m via foldr' yields f m (1, n) as in the generator case: foldr' Q f hf n (ι_Q m) = f m (1, n).
Русский
Для генератора m ∈ M свёртка по ι_Q m в foldr' даёт f m (1, n).
LaTeX
$$$\\foldr'_Q f hf n (\\iota_Q m) = f m (1, n)$$$
Lean4
@[elab_as_elim]
theorem left_induction {P : CliffordAlgebra Q → Prop} (algebraMap : ∀ r : R, P (algebraMap _ _ r))
(add : ∀ x y, P x → P y → P (x + y)) (ι_mul : ∀ x m, P x → P (ι Q m * x)) : ∀ x, P x :=
by
refine reverse_involutive.surjective.forall.2 ?_
intro x
induction x using CliffordAlgebra.right_induction with
| algebraMap r => simpa only [reverse.commutes] using algebraMap r
| add _ _ hx hy => simpa only [map_add] using add _ _ hx hy
| mul_ι _ _ hx => simpa only [reverse.map_mul, reverse_ι] using ι_mul _ _ hx
