mathlib3

2705404e - refactor(linear_algebra/basic): extract content about linear_map.general_linear_group (#18345)