English
The evaluation of foldr'Aux on a given m and x_fx yields a pair whose first component is ι_Q m multiplied by x (in the Clifford sense) and whose second component is f m applied to x_fx.
Русский
Свёртка foldr'Aux на заданных m и x_fx дает пару, первая компонента которой — ι_Q m умноженный на x (клиффордовское произведение), а вторая — f m применено к x_fx.
LaTeX
$$$foldr'Aux\\ Q\\ f\\ m\\ x_{fx} = (ι_Q m * x, f m x_fx)$$$
Lean4
theorem foldr'_ι_mul (f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N)
(hf : ∀ m x fx, f m (ι Q m * x, f m (x, fx)) = Q m • fx) (n m) (x) :
foldr' Q f hf n (ι Q m * x) = f m (x, foldr' Q f hf n x) :=
by
dsimp [foldr']
rw [foldr_mul, foldr_ι, foldr'Aux_apply_apply]
refine congr_arg (f m) (Prod.mk.eta.symm.trans ?_)
congr 1
induction x using CliffordAlgebra.left_induction with
| algebraMap r => simp_rw [foldr_algebraMap, Prod.smul_mk, Algebra.algebraMap_eq_smul_one]
| add x y hx hy => rw [map_add, Prod.fst_add, hx, hy]
| ι_mul m x hx => rw [foldr_mul, foldr_ι, foldr'Aux_apply_apply, hx]
