English
For a linear map F, the symmetry of the alternatingMapLinearEquiv symm applied to F agrees with the corresponding Alt-map evaluation.
Русский
Для линейного отображения F симметрированное применение alternatingMapLinearEquiv.symm к F соответствует оценке чередующейся карты.
LaTeX
$$$$AlternatingMapLinearEquiv.symm(F)(m) = AlternatingMap.instFunLike.coe(F.compAlternatingMap(ιMulti R n))(m)$$$$
Lean4
/-- The linear equivalence ` ⋀[R]^0 M ≃ₗ[R] R`. -/
@[simps! -isSimp symm_apply]
noncomputable def zeroEquiv : ⋀[R]^0 M ≃ₗ[R] R :=
LinearEquiv.ofLinear (alternatingMapLinearEquiv (AlternatingMap.constOfIsEmpty R _ _ 1))
{ toFun := fun r ↦ r • (ιMulti _ _ (by rintro ⟨i, hi⟩; simp at hi))
map_add' := by intros; simp only [add_smul]
map_smul' := by intros; simp only [smul_eq_mul, mul_smul, RingHom.id_apply] } (by aesop) (by aesop)
