Commit 2024-12-13 07:53 f69c743b

View on Github →

feat: representatives for the FixedDetMatrices under SL action (#16160) Define the set of representatives under the action of SL(2, ZZ) and give some reduction lemmas that are useful for later proving that SL(2, ZZ) is generated by S, T.

Estimated changes

Modified Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean

added theorem FixedDetMatrices.S_smul_four

added theorem FixedDetMatrices.T_S_rel_smul

added theorem FixedDetMatrices.ext'

added theorem FixedDetMatrices.ext

added theorem FixedDetMatrices.induction_on

added def FixedDetMatrices.reduce

added def FixedDetMatrices.reduceStep

added theorem FixedDetMatrices.reduce_mem_reps

added theorem FixedDetMatrices.reduce_of_not_pos

added theorem FixedDetMatrices.reduce_of_pos

added def FixedDetMatrices.reduce_rec

added theorem FixedDetMatrices.reduce_reduceStep

added def FixedDetMatrices.reps

added theorem FixedDetMatrices.reps_entries_le_m'

added theorem FixedDetMatrices.reps_zero_empty

added theorem FixedDetMatrices.smul_coe

added theorem FixedDetMatrices.smul_def

deleted theorem FixedDetMatrix.ext'

deleted theorem FixedDetMatrix.ext

deleted theorem FixedDetMatrix.smul_coe

deleted theorem FixedDetMatrix.smul_def

Modified Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean

added theorem ModularGroup.T_S_rel