Theorems · Theorem · group theory

Matrix.GeneralLinearGroup.isParabolic_iff_of_upperTriangular_of_det

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

Specialized version of isParabolic_iff_of_upperTriangular intended for use with discrete subgroups of GL(2, ℝ).

Defined in: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Cited by: 1 results in Mathlib
Foundations: Depth 133 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field LinearOrder IsStrictOrderedRing

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites36

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
LinearOrderstatement and proof · cited by 8,572
Fieldstatement and proof · cited by 7,404
Matrixstatement and proof · cited by 4,303
MonoidHomstatement · cited by 3,629
Unitsstatement · cited by 2,804
IsStrictOrderedRingstatement and proof · cited by 2,490
Units.valstatement and proof · cited by 1,966
Nat.cast_zeroproof · cited by 1,870
LT.lt.ne'proof · cited by 1,417
neg_negproof · cited by 960
Matrix.vecConsproof · cited by 852

Cited by1

Results whose statement or proof uses this declaration.

Subgroup.HasDetPlusMinusOne.isParabolic_iff_of_upperTriangularproof · cited by 1