def lower_triangular (F : Type u) [Field F] [DecidableEq F] (a c d : F) : Matrix.SpecialLinearGroup (Fin 2) F

Equations

• lower_triangular F a c d = if h : a * d = 1 then ⟨!![a, 0; c, d], ⋯⟩ else 1

theorem mem_H_iff_lower_triangular (F : Type u) [Field F] [DecidableEq F] {x : Matrix.SpecialLinearGroup (Fin 2) F} : x ∈ SpecialSubgroups.L F ↔ ∃ (a : F) (c : F) (d : F), a * d = 1 ∧ ↑x = !![a, 0; c, d]

theorem mem_H_iff_lower_triangular' (F : Type u) [Field F] [DecidableEq F] {x : Matrix.SpecialLinearGroup (Fin 2) F} : x ∈ SpecialSubgroups.L F ↔ ∃ (a : F) (c : F) (d : F), !![a, 0; c, d] = ↑x

theorem normalizer_subgroup_T_leq_H (F : Type u) [Field F] [DecidableEq F] {T₀ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)} (hT₀ : 1 < Nat.card ↥T₀) (h : T₀ ≤ SpecialSubgroups.S F) : T₀.normalizer ≤ SpecialSubgroups.L F

theorem normalizer_subgroup_D_eq_DW (F : Type u) [Field F] {D₀ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)} (hD₀ : 2 < Nat.card ↥D₀) (D₀_leq_D : D₀ ≤ SpecialSubgroups.D F) : D₀.normalizer ≤ SpecialSubgroups.DW F