foldr_reverse — Mathlib

English

For Q a quadratic form and a compatible f, folding over the reverse of x with foldr gives the left-fold equivalent: foldr Q f hf n (reverse x) = foldl Q f hf n x.

Русский

Для Q и совместимого f свёртка по reverse x через foldr даёт эквивалент левой свёртке: foldr Q f hf n (reverse x) = foldl Q f hf n x.

LaTeX

$$$\\foldr_Q f hf n (\\text{reverse } x) = \\foldl_Q f hf n x$$$

Lean4

@[simp]
theorem foldr_reverse (f : M →ₗ[R] N →ₗ[R] N) (hf) (n : N) (x : CliffordAlgebra Q) :
    foldr Q f hf n (reverse x) = foldl Q f hf n x :=
  rfl

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