English
There is a linear equivalence between alternating maps M → N and linear maps from wedge^n_R M to N, realized by alternatingMapLinearEquiv.
Русский
Существует линейное эквивалентное отображение между чередующимися отображениями M → N и линейными отображениями из ⋀^n_R M в N посредством alternatingMapLinearEquiv.
LaTeX
$$$\\text{alternatingMapLinearEquiv} : (M [⋀^Fin n]→_R N) ≃_l_R (⋀[R]^n M →_l_R N)$$$
Lean4
@[simp]
theorem map_apply_ιMulti (f : M →ₗ[R] N) (m : Fin n → M) : map n f (ιMulti R n m) = ιMulti R n (f ∘ m) := by
simp only [map, alternatingMapLinearEquiv_apply_ιMulti, AlternatingMap.compLinearMap_apply, Function.comp_def]