Commit 2023-05-30 03:49 bd654783
View on Github →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.