feat: generators for SL(2, Z)

[CBirkbeck]

We show that SL(2, Z) is generated by S and T.

---

• depends on: [Merged by Bors] - feat: matrices with fixed determinant #16159
• depends on : feat: representatives for the FixedDetMatrices under SL action #16160

[github-actions]

PR summary 33482b1059

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.LinearAlgebra.Matrix.FixedDetMatrices	1182

---

Declarations diff

+ A_a_ne_zero
+ A_c_eq_zero
+ A_d_ne_zero
+ FixedDetMatrices
+ S_T_subgroup
+ S_mem_S_T_subgroup
+ S_mul_S_eq
+ S_smul_four
+ SpecialLinearGroup.SL2Z_generators
+ T_S_rel
+ T_mem_S_T_subgroup
+ det_one_mem_S_T_subgroup
+ ext
+ ext'
+ induction_on
+ instance (m : R) : HSMul (SpecialLinearGroup n R) (FixedDetMatrices n R m)
+ instance (m : R) : MulAction (SpecialLinearGroup n R) (FixedDetMatrices n R m)
+ reduce
+ reduce_aux
+ reduce_eqn1
+ reduce_eqn2
+ reduce_eqn3
+ reduce_mem_reps
+ reduce_rec
+ reduce_step
+ reps
+ reps_entries_le_m'
+ reps_fintype
+ reps_one_id
+ reps_zero_is_empty
+ smul_coe
+ smul_def

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat: matrices with fixed determinant #16159
  By Dependent Issues (🤖). Happy coding!