Commit 2020-02-08 10:42 2e18388b

feat(linear_algebra): The Special linear group SL(n, R) (#1960)

• Define the special linear group
• Make definitions independent of PR #1959 That PR changes det_mul to have another, still definitionally equal, type. If the invocations to det_mul are independent of syntactic equality, i.e. we only pass det_mul to erw, this branch should be compatible with the state before the change and after.
• Documentation and code style improvements
• Improve module docstring
• Fix documentation matrix.special_linear_group is not a set but a type Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
• Don't directly coerce from SL to linear maps Now we coerce from matrix.special_linear_group n R to matrix n n R instead of general_linear_group R (n -> R)
• Whitespace fixes
• Fix failing build in src/linear_algebra/dual.lean
• Give an almost generic formula for det_adjugate
• Move det_eq_one_of_card_eq_zero to the correct section
• Replace the ad-hoc assumption of det_adjugate_of_invertible with is_unit
• Fix linting error There was an unnecessary assumption [decidable_eq α] floating around
• Replace special_linear_group.val with the appropriate coercions
• whitespace Correctly indent continued line Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
• Docstrings for the det_adjugate_of_... lemmas