mathlib

bba84730 - feat(linear_algebra): Matrix inverses for square nonsingular matrices (#1816)

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 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>