Commit 2024-11-27 08:00 8a7a0b7d

View on Github →

refactor(LinearAlgebra/Matrix/GeneralLinearGroup): Redefine Matrix.SpecialLinearGroup.toGLand remove duplicate toLinear (#19523) This PR redefines Matrix.SpecialLinearGroup.toGL, as the multiplicative map from the matrix group $$\mathrm{SL}_n(R)$$ to the matrix group $$\mathrm{GL}_n(R)$$, following a Zulip discussion. It also removes a duplicate of Matrix.GeneralLinearGroup.toLin.

Estimated changes

Modified Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

Modified Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean

added theorem Matrix.GeneralLinearGroup.coe_toLin

deleted theorem Matrix.GeneralLinearGroup.coe_toLinear

added theorem Matrix.GeneralLinearGroup.toLin_apply

deleted def Matrix.GeneralLinearGroup.toLinear

deleted theorem Matrix.GeneralLinearGroup.toLinear_apply

deleted def Matrix.SpecialLinearGroup.coeToGL

added def Matrix.SpecialLinearGroup.toGL

Modified Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean

deleted theorem Matrix.SpecialLinearGroup.coe_toGL

deleted def Matrix.SpecialLinearGroup.toGL

Modified Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean

Modified Mathlib/NumberTheory/Modular.lean