The modular-group generator in special linear groups

This module records the matrix of the standard modular-group generator after scalar extension from SL₂(ℤ) to SL₂(R).

Main declaration

• TauCeti.Matrix.SpecialLinearGroup.coe_modularGroup_S: the scalar extension of ModularGroup.S has matrix !![0, -1; 1, 0].

theorem TauCeti.Matrix.SpecialLinearGroup.coe_modularGroup_S {R : Type u} [CommRing R] : ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom R)) ModularGroup.S) = !![0, -1; 1, 0]

The scalar extension of ModularGroup.S to a commutative ring has its standard matrix.