foldl_algebraMap — Mathlib

English

Let Q be a quadratic form. For f as above and any r ∈ R, folding over algebraMap_R(r) via foldr' yields r acting on n. Specifically, foldr' Q f hf n (algebraMap R _ r) = r · n.

Русский

Пусть Q – квадратичная форма; для f и любого r ∈ R свёртка по algebraMap_R(r) в foldr' даёт действие r на n:foldr' Q f hf n (algebraMap R _ r) = r · n.

LaTeX

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

Lean4

@[simp]
theorem foldl_algebraMap (f : M →ₗ[R] N →ₗ[R] N) (hf) (n : N) (r : R) : foldl Q f hf n (algebraMap R _ r) = r • n := by
  rw [← foldr_reverse, reverse.commutes, foldr_algebraMap]

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