2024-11-27 08:00
Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean
refactor(LinearAlgebra/Matrix/GeneralLinearGroup): Redefine `Matrix.SpecialLinearGroup.toGL`and remove duplicate `toLinear` (#19523) …
Added Matrix.GeneralLinearGroup.coe_toLin