Commit 2024-10-28 15:32 c0749f64

View on Github →

feat: matrices with fixed determinant (#16159) Define the set of matrices with fixed determinant and give then an action by SL(2, ZZ).

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean

added theorem FixedDetMatrix.ext'

added theorem FixedDetMatrix.ext

added theorem FixedDetMatrix.smul_coe

added theorem FixedDetMatrix.smul_def

added def FixedDetMatrix

Modified Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean

added theorem ModularGroup.S_mul_S_eq