Commit 2024-04-04 18:16 25e680d5
View on Github →chore(Data/Matrix): add explicit of typecasts (#11593)
This adds some missing Matrix.of typecasts, and uses Matrix.submatrix in places where this is more reasonable than adding of.
Matrix.det_permute' is a new lemma that fills the obvious gap that these submatrix restatements emphasize.