English
The determinant of a family of vectors with respect to a basis e: ι → M defines an alternating linear map on M, assigning a scalar in the base ring.
Русский
Детерминант семейства векторов относительно базиса e задаётAlternatingMap на M, возвращая скаляр в базовом кольце.
LaTeX
$$$\text{Module.Basis.det}: M [⋀^ι]\to_R R$$$
Lean4
/-- The determinant of a family of vectors with respect to some basis, as an alternating
multilinear map. -/
nonrec def det : M [⋀^ι]→ₗ[R] R
where
toMultilinearMap :=
MultilinearMap.mk' (fun v ↦ det (e.toMatrix v))
(fun v i x y ↦ by simp only [e.toMatrix_update, map_add, Finsupp.coe_add, det_updateCol_add])
(fun u i c x ↦ by
simp only [e.toMatrix_update, Algebra.id.smul_eq_mul, LinearEquiv.map_smul]
apply det_updateCol_smul)
map_eq_zero_of_eq' := by
intro v i j h hij
dsimp
rw [← Function.update_eq_self i v, h, ← det_transpose, e.toMatrix_update, ← updateRow_transpose, ←
e.toMatrix_transpose_apply]
apply det_zero_of_row_eq hij
rw [updateRow_ne hij.symm, updateRow_self]
