English
Let Q be a quadratic form on M. For a bilinear map f and accumulator n, folding over a product a b in the Clifford algebra equals folding first over a then b with a shifted accumulator: foldl Q f hf n (a b) = foldl Q f hf (foldl Q f hf n a) b.
Русский
Пусть Q – квадратичная форма; для f и накопителя n свёртка по произведению a b равна свёртке сначала по a, затем по b: foldl Q f hf n (a b) = foldl Q f hf (foldl Q f hf n a) b.
LaTeX
$$$\\foldl_Q f hf n (a b) = \\foldl_Q f hf (\\foldl_Q f hf n a) b$$$
Lean4
@[simp]
theorem foldl_mul (f : M →ₗ[R] N →ₗ[R] N) (hf) (n : N) (a b : CliffordAlgebra Q) :
foldl Q f hf n (a * b) = foldl Q f hf (foldl Q f hf n a) b := by
rw [← foldr_reverse, ← foldr_reverse, ← foldr_reverse, reverse.map_mul, foldr_mul]
