Commit 2021-04-24 19:36 8f8b194a

feat(linear_algebra): Lagrange formulas for expanding det along a row or column (#6897) This PR proves the full Lagrange formulas for writing the determinant of a n+1 × n+1 matrix as an alternating sum of minors. @pechersky and @eric-wieser already put together enough of the pieces so that simp could apply this formula to matrices of a known size. In the end I still had to apply a couple of permutations (fin.cycle_range defined in #6815) to the entries to get to the "official" formula.