alternatingMapLinearEquiv_apply_ιMulti

English

For any alternating map f, the value of the linear equivalence on ιMulti is f evaluated on its argument.

Русский

Для любой чередующейся карты f значение линейного эквивалента на ιMulti равно f, применённому к его аргументу.

LaTeX

$$$\\text{alternatingMapLinearEquiv}(f)(\\iotaMulti(R,n)(a)) = f(a)$$$

Lean4

@[simp]
theorem alternatingMapLinearEquiv_apply_ιMulti (f : M [⋀^Fin n]→ₗ[R] N) (a : Fin n → M) :
    alternatingMapLinearEquiv f (ιMulti R n a) = f a :=
  DFunLike.congr_fun (alternatingMapLinearEquiv_comp_ιMulti f) a

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