English
Let Q be a quadratic form on M. For f with hf, folding over ι_Q m multiplied by x satisfies a recursion: foldr'_ι_mul Q f hf n (ι_Q m * x) = f m (x, foldr' Q f hf n x).
Русский
Пусть Q – квадратичная форма; для f с hf свёртка по ι_Q m, умножения на x удовлетворяет рекурсивному правилу: foldr'_ι_mul Q f hf n (ι_Q m · x) = f m (x, foldr' Q f hf n x).
LaTeX
$$$\\foldr'_ι_mul\\ Q\\ f\\ hf\\ n (\\iota_Q m * x) = f m (x, \\foldr'\\ Q\\ f\\ hf\\ n\\ x)$$$
Lean4
/-- Auxiliary definition for `CliffordAlgebra.foldr'` -/
def foldr'Aux (f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N) : M →ₗ[R] Module.End R (CliffordAlgebra Q × N) :=
by
have v_mul := (Algebra.lmul R (CliffordAlgebra Q)).toLinearMap ∘ₗ ι Q
have l := v_mul.compl₂ (LinearMap.fst _ _ N)
exact
{ toFun := fun m => (l m).prod (f m)
map_add' := fun v₂ v₂ =>
LinearMap.ext fun x => Prod.ext (LinearMap.congr_fun (l.map_add _ _) x) (LinearMap.congr_fun (f.map_add _ _) x)
map_smul' := fun c v =>
LinearMap.ext fun x =>
Prod.ext (LinearMap.congr_fun (l.map_smul _ _) x) (LinearMap.congr_fun (f.map_smul _ _) x) }
