mathlib

d07e3b3e - feat(linear_algebra/basic): general_linear_group basics (#1064)

feat(linear_algebra/basic): general_linear_group basics (#1064) * feat(linear_algebra/basic): general_linear_group basics This patch proves that the general_linear_group (defined as units in the endomorphism ring) are equivalent to the group of linear equivalences. * shorten proof of ext * Add mul_equiv * Use coe * Fix stupid error