mathlib3

35d574e3 - feat(linear_algebra/determinant): alternating maps as multiples of determinant (#10233)

feat(linear_algebra/determinant): alternating maps as multiples of determinant (#10233) Add the lemma that any alternating map with the same type as the determinant map with respect to a basis is a multiple of the determinant map (given by the value of the alternating map applied to the basis vectors).