foldr'_algebraMap — Mathlib

English

Under hf, folding over the product ι_Q m · x yields f m (x, foldr' Q f hf n x), describing how the auxiliary fold interacts with left multiplication by generators.

Русский

При hf свёртка над произведением ι_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

theorem foldr'_algebraMap (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 r) : foldr' Q f hf n (algebraMap R _ r) = r • n :=
  congr_arg Prod.snd (foldr_algebraMap _ _ _ _ _)

Похожие утверждения