Theorems · Theorem · number theory

Subgroup.HasDetPlusMinusOne.isParabolic_iff_of_upperTriangular

∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {𝒢 : Subgroup (GL (Fin 2) K)}
  [𝒢.HasDetPlusMinusOne] {g : GL (Fin 2) K},
  g ∈ 𝒢 →
    ↑g 1 0 = 0 →
      (g.IsParabolic ↔
        (∃ x, x ≠ 0 ∧ g = Matrix.GeneralLinearGroup.upperRightHom x) ∨
          ∃ x, x ≠ 0 ∧ g = -Matrix.GeneralLinearGroup.upperRightHom x)

Defined in

Mathlib.NumberTheory.ModularForms.Cusps

Cited by

1 results in Mathlib

Foundations

Depth 134 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldLinearOrderIsStrictOrderedRingSubgroup.HasDetPlusMinusOne