Zulip Chat Archive

Stream: Is there code for X?

Topic: General linear groups


view this post on Zulip Kirby Sikes (Feb 21 2020 at 23:10):

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

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

view this post on Zulip Alex J. Best (Feb 21 2020 at 23:19):

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!

view this post on Zulip Kirby Sikes (Feb 21 2020 at 23:20):

Thanks!


Last updated: May 16 2021 at 05:21 UTC