S — Mathlib · SciLib

English

The element S in SL(2,Z) corresponds to the matrix [[0,-1],[1,0]].

Русский

Элемент S в SL(2,Z) соответствует матрице [[0,-1],[1,0]].

LaTeX

$$↑S = !![0, -1; 1, 0]$$

Lean4

/-- The matrix `S = [[0, -1], [1, 0]]` as an element of `SL(2, ℤ)`.

This element acts naturally on the Euclidean plane as a rotation about the origin by `π / 2`.

This element also acts naturally on the hyperbolic plane as rotation about `i` by `π`. It
represents the Mobiüs transformation `z ↦ -1/z` and is an involutive elliptic isometry. -/
def S : SL(2, ℤ) :=
  ⟨!![0, -1; 1, 0], by simp [Matrix.det_fin_two_of]⟩

Похожие утверждения