English
Let Q be a quadratic form on M. For a bilinear map f compatible with the Clifford relations, folding over a product a · b in the Clifford algebra equals folding over b first and then a, i.e., foldr Q f hf n (a b) = foldr Q f hf (foldr Q f hf n b) a.
Русский
Пусть Q – квадратичная форма на M. Для билинеарного отображения f, согласованного с клиффордовым отношением, свёртка по произведению a b равна свёртке по b, затем по a: foldr Q f hf n (a b) = foldr Q f hf (foldr Q f hf n b) a.
LaTeX
$$$\\foldr_Q f hf n (a b) = \\foldr_Q f hf (\\foldr_Q f hf n b)\\, a$$$
Lean4
@[simp]
theorem foldr_mul (f : M →ₗ[R] N →ₗ[R] N) (hf) (n : N) (a b : CliffordAlgebra Q) :
foldr Q f hf n (a * b) = foldr Q f hf (foldr Q f hf n b) a :=
LinearMap.congr_fun (map_mul (lift Q _) _ _) n
