Stream: Is there code for X?
Topic: General linear groups
Kirby Sikes (Feb 21 2020 at 23:10):
It seems likely that this exists, but I haven't found it. Thanks.
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!
Kirby Sikes (Feb 21 2020 at 23:20):
Last updated: May 16 2021 at 05:21 UTC