ιMulti_span_fixedDegree — Mathlib

English

For f: ∀ i, M [⋀^Fin i]→ₗ[R] N and v: Fin n → M, the evaluation of liftAlternating on the i-ary family at v equals the evaluation of the nth alternating map on v; i.e., liftAlternating(f) evaluated at v equals f n evaluated at v.

Русский

Для f: ∀ i, M [⋀^Fin i]→ₗ[R] N и v: Fin n → M, значение liftAlternating на v эквивалентно значению f n на v.

LaTeX

$$$\text{liftAlternating}(f)(v) = f\,n\,v$$$

Lean4

/-- The image of `ExteriorAlgebra.ιMulti R n` spans the `n`th exterior power. Variant of
`ExteriorAlgebra.ιMulti_span_fixedDegree`, useful in rewrites. -/
theorem ιMulti_span_fixedDegree : Submodule.span R (Set.range (ExteriorAlgebra.ιMulti R n)) = ⋀[R]^n M :=
  ExteriorAlgebra.ιMulti_span_fixedDegree R n

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