Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

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

Merged
merged 40 commits into from
Jan 27, 2020
Merged

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

merged 40 commits into from
Jan 27, 2020

Commits on Jan 27, 2020

  1. Small lemmata on transpose

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    d5425cc View commit details
    Browse the repository at this point in the history

  2. WIP: some work on inverse matrices

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    d49a280 View commit details
    Browse the repository at this point in the history

  3. Prove that some matrices have inverses

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    c508497 View commit details
    Browse the repository at this point in the history

  4. Finish the proof: show that the determinant is 0 if a column is repeated

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    bf3eaa6 View commit details
    Browse the repository at this point in the history

  5. Show that nonsingular_inv is also a right inverse

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    9196a21 View commit details
    Browse the repository at this point in the history

  6. Cleanup and code movement

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    a50c72a View commit details
    Browse the repository at this point in the history

  7. Code cleanup and documentation

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    1ae96a6 View commit details
    Browse the repository at this point in the history

  8. More cleanup and documentation

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    802c4ec View commit details
    Browse the repository at this point in the history

  9. Generalize det_zero_of_column_eq to remove the linear order assumption

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    f91d847 View commit details
    Browse the repository at this point in the history

  10. Fix linting issues.

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    9242b03 View commit details
    Browse the repository at this point in the history

  11. Unneeded import can be removed

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    db49d64 View commit details
    Browse the repository at this point in the history

  12. A little bit more cleanup

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    d146ead View commit details
    Browse the repository at this point in the history

  13. Generalize nonsing_inv to any ring with inverse

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    078d28b View commit details
    Browse the repository at this point in the history

  14. Improve comments for nonsingular_inverse

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    06d5e1f View commit details
    Browse the repository at this point in the history

  15. Remove the less general det_zero_of_column_eq_of_char_ne_two proof

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    0176199 View commit details
    Browse the repository at this point in the history

  16. Rename cramer_map_val -> cramer_map_def 

    Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
    @Vierkantor @ChrisHughes24
    Vierkantor and ChrisHughes24 committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    a605cb0 View commit details
    Browse the repository at this point in the history

  17. whitespace 

    Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
    @Vierkantor @ChrisHughes24
    Vierkantor and ChrisHughes24 committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    59f65c8 View commit details
    Browse the repository at this point in the history

  18. whitespace: indent tactic proofs

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    867feb3 View commit details
    Browse the repository at this point in the history

  19. More renaming cramer_map_val -> cramer_map_def

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    7d6f5fc View commit details
    Browse the repository at this point in the history

  20. swap_mul_self_mul can be a simp lemma

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    7d32651 View commit details
    Browse the repository at this point in the history

  21. Make parameter σ to swap_mul_eq_iff implicit

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    ea9be5e View commit details
    Browse the repository at this point in the history

  22. Update usage of function.update_same and function.update_noteq

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    fbd8af6 View commit details
    Browse the repository at this point in the history

  23. 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.
    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    0ead3d4 View commit details
    Browse the repository at this point in the history

  24. Re-introduce matrix.det_permute (now based on `matrix.det_permutati… 

    …on`)
    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    bfdc2cd View commit details
    Browse the repository at this point in the history

  25. Delete cramer_at and clean up the proofs depending on it

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    bfccd9e View commit details
    Browse the repository at this point in the history

  26. Replace cramer_map with cramer after defining cramer

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    d5ccd12 View commit details
    Browse the repository at this point in the history

  27. Apply suggestions from code review 

    Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>
    @Vierkantor @sgouezel
    Vierkantor and sgouezel committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    8057b7c View commit details
    Browse the repository at this point in the history

  28. Clean up imports

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    6bc4b7a View commit details
    Browse the repository at this point in the history

  29. Formatting: move } to previous lines

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    b02933a View commit details
    Browse the repository at this point in the history

  30. Move assumptions of det_zero_of_repeated_column from variable to ar… 

    …gument
    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    1cc4827 View commit details
    Browse the repository at this point in the history

  31. whitespace 

    Insert space between `finset.filter` and the filter condition.

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>
    @Vierkantor @sgouezel
    Vierkantor and sgouezel committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    d0c0d38 View commit details
    Browse the repository at this point in the history

  32. Improve docstrings

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    b9b5d1b View commit details
    Browse the repository at this point in the history

  33. Make argument to prod_cancels_of_partition_cancels explicit

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    1e163a9 View commit details
    Browse the repository at this point in the history

  34. Rename replace_column and replace_row to update_column and `upd… 

    …ate_row`
    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    608f853 View commit details
    Browse the repository at this point in the history

  35. Replace update_column_eq with update_column_self + rewriting step

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    21d6b55 View commit details
    Browse the repository at this point in the history

  36. whitespace 

    Newlines between all lemmas
    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    7a275ab View commit details
    Browse the repository at this point in the history

  37. whitespace 

    Newline before 'begin'
    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    9dc30e9 View commit details
    Browse the repository at this point in the history

  38. Fix conflicts with latest mathlib

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    3a44403 View commit details
    Browse the repository at this point in the history

  39. Remove unnecessary explicitification of arguments

    @Vierkantor
    Vierkantor committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    7cdd1f4 View commit details
    Browse the repository at this point in the history

  40. Merge branch 'master' into matrix_inverse

    @mergify
    mergify[bot] committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    9a065c8 View commit details
    Browse the repository at this point in the history