forked from leanprover-community/mathlib3
-
Notifications
You must be signed in to change notification settings - Fork 0
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): Matrix inverses for square nonsingular matrices (…
…leanprover-community#1816) * Prove that some matrices have inverses * Finish the proof: show that the determinant is 0 if a column is repeated * Show that nonsingular_inv is also a right inverse * Cleanup and code movement * Small lemmata on transpose * WIP: some work on inverse matrices * Code cleanup and documentation * More cleanup and documentation * Generalize det_zero_of_column_eq to remove the linear order assumption * Fix linting issues. * Unneeded import can be removed * A little bit more cleanup * Generalize nonsing_inv to any ring with inverse * Improve comments for `nonsingular_inverse` * Remove the less general `det_zero_of_column_eq_of_char_ne_two` proof * Rename `cramer_map_val` -> `cramer_map_def` Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> * whitespace Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> * whitespace: indent tactic proofs * More renaming `cramer_map_val` -> `cramer_map_def` * `swap_mul_self_mul` can be a `simp` lemma * Make parameter σ to `swap_mul_eq_iff` implicit * Update usage of `function.update_same` and `function.update_noteq` * Replace `det_permute` with `det_permutation` Although the statement now gives the determinant of a permutation matrix, the proof is easier if we write it as a permuted identity matrix. Thus the proof is basically the same, except a different line showing that the entries are the same. * Re-introduce `matrix.det_permute` (now based on `matrix.det_permutation`) * Delete `cramer_at` and clean up the proofs depending on it * Replace `cramer_map` with `cramer` after defining `cramer` * Apply suggestions from code review Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr> * Clean up imports * Formatting: move } to previous lines * Move assumptions of `det_zero_of_repeated_column` from variable to argument * whitespace Insert space between `finset.filter` and the filter condition. Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr> * Improve docstrings * Make argument to `prod_cancels_of_partition_cancels` explicit * Rename `replace_column` and `replace_row` to `update_column` and `update_row` * Replace `update_column_eq` with `update_column_self` + rewriting step * whitespace Newlines between all lemmas * whitespace Newline before 'begin' * Fix conflicts with latest mathlib * Remove unnecessary explicitification of arguments Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
- Loading branch information
Showing
8 changed files
with
508 additions
and
9 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
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
Oops, something went wrong.