mathlib3

8f8b194a - feat(linear_algebra): Lagrange formulas for expanding `det` along a row or column (#6897)

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. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>