map_id — Mathlib

English

Fixing the first argument m ∈ M, the (n+1)-ary exterior product map is equal to the left multiplication by ι_R(m) composed with the n-ary map: (ιMulti R (n+1)).curryLeft m = (ι_R m) · (ιMulti R n).

Русский

При фиксировании первого аргумента m ∈ M, (n+1)-арное внешнее произведение равно левой умножении на ι_R(m), затем применению n-арного отображения.

LaTeX

$$$ (ιMulti\\_R(n+1)).curryLeft(m) = (ι_R(m)) \\cdot (ιMulti\\_R(n)). $$$

Lean4

@[simp]
theorem map_id : map LinearMap.id = AlgHom.id R (ExteriorAlgebra R M) :=
  CliffordAlgebra.map_id 0

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