chore(linear_algebra/special_linear_group): Cleanup and golf (#8569)
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`.





leanprover-community/mathlib,leanprover-community/mathlib