Commit 2020-01-27 20:50 bba84730

feat(linear_algebra): Matrix inverses for square nonsingular matrices (#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