Commit 2025-10-15 06:00 60c559f1

View on Github →

feat(GeneralLinearGroup/FinTwo): the addChar sending x to [1,x;0,1] (#30475)

Estimated changes

Modified Mathlib/Algebra/Group/AddChar.lean

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

added theorem Matrix.GeneralLinearGroup.injective_upperRightHom

added theorem Matrix.GeneralLinearGroup.isParabolic_iff_of_upperTriangular

added theorem Matrix.GeneralLinearGroup.isParabolic_iff_of_upperTriangular_of_det

added def Matrix.GeneralLinearGroup.upperRightHom

added theorem Matrix.isParabolic_iff_of_upperTriangular

Modified Mathlib/NumberTheory/ModularForms/Cusps.lean

added theorem Subgroup.HasDetPlusMinusOne.isParabolic_iff_of_upperTriangular

Modified Mathlib/Topology/Instances/Matrix.lean

added theorem Matrix.GeneralLinearGroup.continuous_upperRightHom