reps_one_id — Mathlib

English

Under certain determinant 1 and entry constraints, a representative A in reps(1) must be the identity element in SL(2, Z).

Русский

При определённых ограничениях на детерминант и элементы, представитель A в reps(1) должен быть единицей в SL(2, Z).

LaTeX

$$$A = 1 \quad\text{in } SL(2, \mathbb{Z})$ under the given conditions.$$

Lean4

theorem reps_one_id (A : FixedDetMatrix (Fin 2) ℤ 1) (a1 : A.1 1 0 = 0) (a4 : 0 < A.1 0 0)
    (a6 : |A.1 0 1| < |(A.1 1 1)|) : A = (1 : SL(2, ℤ)) :=
  by
  have := Int.mul_eq_one_iff_eq_one_or_neg_one.mp (A_c_eq_zero a1)
  ext i j
  fin_cases i <;> fin_cases j <;> aesop

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