General linear groups

Stream: Is there code for X?

[Kirby Sikes]

https://en.wikipedia.org/wiki/General_linear_group

It seems likely that this exists, but I haven't found it. Thanks.

[Alex J. Best]

It's in linear_algebra/basic.lean see https://leanprover-community.github.io/mathlib_docs/linear_algebra/basic.html#linear_map.general_linear_group there isn't a huge amount, but we have that it exists and is a group!

[Kirby Sikes]

Thanks!