English
The special linear group SL2(Z) is generated by the matrices S and T; i.e., every element of SL2(Z) can be expressed as a finite product of S and T (the subgroup generated by S and T equals the whole group).
Русский
Группа SL2(Z) порождается матрицами S и T; то есть каждый элемент SL2(Z) представим как конечное произведение S и T (подгруппа, порождаемая S и T, равна всей группе).
LaTeX
$$$\mathrm{SL}_2(\mathbb{Z}) = \langle S, T \rangle$$$
Lean4
/-- `SL(2, ℤ)` is generated by `S` and `T`. -/
theorem SL2Z_generators : closure { S, T } = ⊤ := by
rw [eq_top_iff']
intro A
induction A using (induction_on one_ne_zero) with
| h0 A a1 a4 _ a6 =>
rw [reps_one_id A a1 a4 a6]
exact one_mem _
| hS B hb => exact mul_mem (subset_closure (Set.mem_insert S { T })) hb
| hT B hb => exact mul_mem (subset_closure (Set.mem_insert_of_mem S rfl)) hb
