foldr'Aux_apply_apply — Mathlib

English

Under hf, the foldr' recursion at the generator ι_Q m matches the bilinear action f m (1, -) on the second component, reflecting how ι_Q m interacts with the auxiliary folding step.

Русский

При hf свёртка по генератору ι_Q m в foldr' согласуется с билинейным действием f m (1, -) на второй компоненту, отражая взаимодействие ι_Q m с дополнительным шагом свёртки.

LaTeX

$$$foldr'_ι Q f hf n (\\iota_Q m) = f m (1, n)$$$

Lean4

theorem foldr'Aux_apply_apply (f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N) (m : M) (x_fx) :
    foldr'Aux Q f m x_fx = (ι Q m * x_fx.1, f m x_fx) :=
  rfl

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