foldr_one — Mathlib

English

Let Q be a quadratic form on M. For a bilinear map f as above, folding with the identity element 1 of the Clifford algebra leaves the vector n unchanged. In symbols, foldr Q f hf n 1 = n.

Русский

Пусть Q – квадратичная форма на M. Для билинеарного отображения f, свёртка по единице Clifford алгебры сохраняет элемент n, т.е. foldr Q f hf n 1 = n.

LaTeX

$$$\\foldr_Q f hf n 1 = n$$$

Lean4

@[simp]
theorem foldr_one (f : M →ₗ[R] N →ₗ[R] N) (hf) (n : N) : foldr Q f hf n 1 = n :=
  LinearMap.congr_fun (map_one (lift Q _)) n

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