Commit 2024-07-05 09:32 b387c548

View on Github →

chore: Split of GeneralLinearGroup (#14439) Split of LinearAlgebra/Matrix/GeneralLinearGroup.lean into LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean and LinearAlgebra/Matrix/GeneralLinearGroup/Basic.lean. This is motivated by PR #14095.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Complex/Isometry.lean

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

Created Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Basic.lean

added def Matrix.planeConformalMatrix

Renamed Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup.lean to Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean

deleted def Matrix.planeConformalMatrix

Modified Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean

Modified Mathlib/NumberTheory/Modular.lean

Modified Mathlib/NumberTheory/ModularForms/SlashActions.lean