Build the idea in three steps
- Put four integers into a two-row table: the first row (a, b) and the second row (c, d), like columns in order. Multiplying points by that table is the transformation.
- The tables counted here have exactly determinant ad − bc = 1 with integer entries; Lean writes SL(2, ℤ) for this family.
- Composing two such tables, or inverting one, always gives a table of the same kind. The Lean vocabulary Subgroup SL(2, ℤ) means a chosen collection that stays closed under those movements.
A small example
The identity table with rows (1, 0) and (0, 1) moves nothing, so it belongs to every such collection.