foldr'Aux_foldr'Aux — Mathlib

English

For the algebraMap from R into CliffordAlgebra(Q) and f with hf, folding over algebraMap_R(r) via foldr' yields r acting on n: foldr'_algebraMap Q f hf n r = r · n.

Русский

Для отображения algebraMap_R из R в CliffordAlgebra(Q) и f с hf, свёртка по алгебраMap даёт действие скаляра r на n: foldr'_algebraMap Q f hf n r = r · n.

LaTeX

$$$\\foldr'_Q f hf n (\\mathrm{algebraMap}_R\\, r) = r \\cdot n$$$

Lean4

theorem foldr'Aux_foldr'Aux (f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N)
    (hf : ∀ m x fx, f m (ι Q m * x, f m (x, fx)) = Q m • fx) (v : M) (x_fx) :
    foldr'Aux Q f v (foldr'Aux Q f v x_fx) = Q v • x_fx :=
  by
  obtain ⟨x, fx⟩ := x_fx
  simp only [foldr'Aux_apply_apply]
  rw [← mul_assoc, ι_sq_scalar, ← Algebra.smul_def, hf, Prod.smul_mk]

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