[Merged by Bors] - feat(linear_algebra/matrix/general_linear_group): GL(n, R)

[CBirkbeck]

added this file which contains definition of the general linear group as well as the subgroup of matrices with positive determinant.

---

[eric-wieser]

Here's the lemma you need to close your sorry:

/-- Applying `matrix.nonsing_inv` to the coercion is the same as coercing the group inverse. -/
lemma nonsing_inv_coe_eq_coe_inv (A : units (matrix n n R)) : (A : matrix n n R)⁻¹ = ↑(A⁻¹) :=
begin
  letI := A.invertible,
  exact (inv_eq_nonsing_inv_of_invertible (A : matrix n n R)).symm,
end

[eric-wieser]

Can you take a look at https://leanprover-community.github.io/contribute/style.html#structuring-definitions-and-theorems and reformat your file appropriately? Specifically, you should:

• Indent lemma bodies by two spaces not one
• avoid more than one blank line in a row
• Ensure parameters are always spaced as (name : type), never (name: type )

[CBirkbeck]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests