foldl_reverse — Mathlib

English

Let Q be a quadratic form on M. For a bilinear map f with the same hf compatibility, folding along the reverse of x using foldl equals folding along x using foldr: foldl Q f hf n (reverse x) = foldr Q f hf n x.

Русский

Пусть Q – квадратичная форма на M. При том же условии совместимости hf свёртка по reverse x с помощью foldl равна свёртке по x с помощью foldr: foldl Q f hf n (reverse x) = foldr Q f hf n x.

LaTeX

$$$\\text{foldl}_Q\\,f\\,hf\\,n (\\text{reverse } x) = \\text{foldr}_Q\\,f\\,hf\\,n\\,x$$$

Lean4

@[simp]
theorem foldl_reverse (f : M →ₗ[R] N →ₗ[R] N) (hf) (n : N) (x : CliffordAlgebra Q) :
    foldl Q f hf n (reverse x) = foldr Q f hf n x :=
  DFunLike.congr_arg (foldr Q f hf n) <| reverse_reverse _

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