Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(linear_algebra): Lagrange formulas for expanding
det
along a r…
…ow 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>
- Loading branch information
1 parent
f83ae59
commit 8f8b194
Showing
4 changed files
with
135 additions
and
10 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters