S_mul_S_eq — Mathlib

English

The standard generator S satisfies S^2 = -I in SL(2, Z), i.e., its square is the negative identity.

Русский

Стандартный генератор S удовлетворяет S^2 = -I в SL(2, Z), то есть квадрат S равен минус единичной матрице.

LaTeX

$$$S^2 = -I_2$$$

Lean4

theorem S_mul_S_eq : (S : Matrix (Fin 2) (Fin 2) ℤ) * S = -1 :=
  by
  simp only [S, Int.reduceNeg, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, vecMul_cons, head_cons, zero_smul,
    tail_cons, neg_smul, one_smul, neg_cons, neg_zero, neg_empty, empty_vecMul, add_zero, zero_add, empty_mul,
    Equiv.symm_apply_apply]
  exact Eq.symm (eta_fin_two (-1))

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