Commit 2021-08-09 13:47 fc694c5b

chore(linear_algebra/special_linear_group): Cleanup and golf (#8569) This cleans up a number things in this file:

• Many lemmas were duplicated between ↑A and ⇑A. This eliminates the latter spelling from all lemmas, and makes it simplify to the former. Unfortunately the elaborator fights us at every step of the way with ↑A, so we introduce local notation to take the pain away.
• Some lemma names did not match the convention established elsewhere
• Some definitions can be bundled more heavily than they currently are. In particular, this merges together to_lin' and to_linear_equiv, as well as to_GL and embedding_GL.