mathlib3

bd654783 - chore(linear_algebra/alternating): make `ι` an explicit arg of `alternating_map.const_of_is_empty` (#19123)

chore(linear_algebra/alternating): make `ι` an explicit arg of `alternating_map.const_of_is_empty` (#19123) While for general multilinear maps one can deduce it from the type of `E : ι -> Type*`, this doesn't work for alternating maps.