@[reducible]

def SimpleGroups.lieAlgebraMatrix (n : ℕ) : LieAlgebra ℝ (Matrix (Fin n) (Fin n) ℝ)

theorem SimpleGroups.lie_bracket_def {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommRing R] (A B : Matrix n n R) : ⁅A, B⁆ = A * B - B * A

noncomputable def SimpleGroups.lieAlgebraSet (m : ℕ) (G : Subgroup (GL (Fin m) ℝ)) : Set (Matrix (Fin m) (Fin m) ℝ)

noncomputable def SimpleGroups.lieAlgebraSetPath (m : ℕ) (G : Subgroup (GL (Fin m) ℝ)) : Set (Matrix (Fin m) (Fin m) ℝ)

noncomputable def SimpleGroups.lieAlgebraSetDual (m : ℕ) (P : Matrix (Fin m) (Fin m) (DualNumber ℝ) → Prop) : Set (Matrix (Fin m) (Fin m) ℝ)

theorem SimpleGroups.lie_algebra_proposition (m : ℕ) (G : Subgroup (GL (Fin m) ℝ)) (P : Matrix (Fin m) (Fin m) (DualNumber ℝ) → Prop) (hP : ∀ (M : (Matrix (Fin m) (Fin m) ℝ)ˣ), M ∈ G ↔ P ((↑M).map TrivSqZeroExt.inl)) : lieAlgebraSet m G = lieAlgebraSetPath m G ∧ lieAlgebraSet m G = lieAlgebraSetDual m P ∧ ∃ (S : Submodule ℝ (Matrix (Fin m) (Fin m) ℝ)), ↑S = lieAlgebraSet m G

structure SimpleGroups.IsOneParameterGroup (m : ℕ) (φ : ℝ → Matrix (Fin m) (Fin m) ℂ) : Prop

• map_zero : φ 0 = 1
• map_add (s t : ℝ) : φ (s + t) = φ s * φ t
• differentiable : Differentiable ℝ φ

theorem SimpleGroups.one_param_subgroup_form (m : ℕ) (φ : ℝ → Matrix (Fin m) (Fin m) ℂ) (hφ : IsOneParameterGroup m φ) : ∃! A : Matrix (Fin m) (Fin m) ℂ, ∀ (t : ℝ), φ t = NormedSpace.exp (↑t • A)

theorem SimpleGroups.su2_matrix_form (M : Matrix (Fin 2) (Fin 2) ℂ) (hU : M ∈ Matrix.specialUnitaryGroup (Fin 2) ℂ) : ∃ (α : ℂ) (β : ℂ), M = !![α, β; -(starRingEnd ℂ) β, (starRingEnd ℂ) α] ∧ Complex.normSq α + Complex.normSq β = 1

@[reducible, inline]

abbrev SimpleGroups.SU2 : Submonoid (Matrix (Fin 2) (Fin 2) ℂ)

theorem SimpleGroups.D_mem_SU2 : !![Complex.I, 0; 0, -Complex.I] ∈ SU2

theorem SimpleGroups.W_mem_SU2 : !![0, 1; -1, 0] ∈ SU2

theorem SimpleGroups.su2_center_mem_iff (M : ↥SU2) : M ∈ Subgroup.center ↥SU2 ↔ ↑M = 1 ∨ ↑M = -1

theorem SimpleGroups.su2_trace_real (M : ↥(Matrix.specialUnitaryGroup (Fin 2) ℂ)) : (↑M).trace.im = 0

theorem SimpleGroups.su2_trace_bound (M : ↥(Matrix.specialUnitaryGroup (Fin 2) ℂ)) : ‖(↑M).trace‖ ≤ 2

noncomputable def SimpleGroups.diagRotation (θ : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

theorem SimpleGroups.diagRotation_add (θ₁ θ₂ : ℝ) : diagRotation θ₁ * diagRotation θ₂ = diagRotation (θ₁ + θ₂)

theorem SimpleGroups.diagRotation_zero : diagRotation 0 = 1

theorem SimpleGroups.diagRotation_mem_SU2 (θ : ℝ) : diagRotation θ ∈ SU2

noncomputable def SimpleGroups.longitudeI : Subgroup ↥SU2

theorem SimpleGroups.diagRotation_periodic (θ : ℝ) (n : ℤ) : diagRotation (θ + ↑n * (2 * Real.pi)) = diagRotation θ

noncomputable def SimpleGroups.diagRotationToLongI (θ : ℝ) : ↥longitudeI

theorem SimpleGroups.diagRotationToLongI_periodic (a b : ℝ) (h : (QuotientAddGroup.leftRel (AddSubgroup.zmultiples (2 * Real.pi))) a b) : diagRotationToLongI a = diagRotationToLongI b

noncomputable def SimpleGroups.longitudeMap : Multiplicative (AddCircle (2 * Real.pi)) →* ↥longitudeI

theorem SimpleGroups.longitude_iso : Function.Bijective ⇑longitudeMap

noncomputable def SimpleGroups.longitudeIMulEquiv : Multiplicative (AddCircle (2 * Real.pi)) ≃* ↥longitudeI

theorem SimpleGroups.su2_normal_contains_all_traces (N : Subgroup ↥(Matrix.specialUnitaryGroup (Fin 2) ℂ)) (hN : N.Normal) (M : ↥(Matrix.specialUnitaryGroup (Fin 2) ℂ)) (hMN : M ∈ N) (hMnc : M ∉ Subgroup.center ↥(Matrix.specialUnitaryGroup (Fin 2) ℂ)) (t : ℝ) : |t| ≤ 2 → ∃ Q ∈ N, (↑Q).trace = ↑t

theorem SimpleGroups.su2_conj_to_diag (A : ↥SU2) : ∃ (D : ↥SU2), (∃ (z : ℂ), z * (starRingEnd ℂ) z = 1 ∧ ↑D = !![z, 0; 0, (starRingEnd ℂ) z]) ∧ IsConj A D

theorem SimpleGroups.su2_trace_conj_inv (P A : ↥SU2) : (↑(P * A * P⁻¹)).trace = (↑A).trace

theorem SimpleGroups.su2_diag_conj_of_trace (D₁ D₂ : ↥SU2) (z₁ z₂ : ℂ) (hz₁ : z₁ * (starRingEnd ℂ) z₁ = 1) (hz₂ : z₂ * (starRingEnd ℂ) z₂ = 1) (hD₁ : ↑D₁ = !![z₁, 0; 0, (starRingEnd ℂ) z₁]) (hD₂ : ↑D₂ = !![z₂, 0; 0, (starRingEnd ℂ) z₂]) (htrace : (↑D₁).trace = (↑D₂).trace) : IsConj D₁ D₂

theorem SimpleGroups.su2_conj_of_trace_eq (A B : ↥(Matrix.specialUnitaryGroup (Fin 2) ℂ)) (h : (↑A).trace = (↑B).trace) : IsConj A B

theorem SimpleGroups.su2_normal_subgroups (N : Subgroup ↥(Matrix.specialUnitaryGroup (Fin 2) ℂ)) (hN : N.Normal) : N = ⊥ ∨ N = ⊤ ∨ N = Subgroup.center ↥(Matrix.specialUnitaryGroup (Fin 2) ℂ)

theorem SimpleGroups.su2_center_ne_top : Subgroup.center ↥(Matrix.specialUnitaryGroup (Fin 2) ℂ) ≠ ⊤

theorem SimpleGroups.su2_mod_center_isSimple : IsSimpleGroup (↥(Matrix.specialUnitaryGroup (Fin 2) ℂ) ⧸ Subgroup.center ↥(Matrix.specialUnitaryGroup (Fin 2) ℂ))

theorem SimpleGroups.exists_sq_not_in_zero_one_neg_one' (F : Type u_1) [Field F] [Fintype F] (hF : 5 < Fintype.card F) : ∃ (r : F), r ^ 2 ≠ 0 ∧ r ^ 2 ≠ 1 ∧ r ^ 2 ≠ -1

def SimpleGroups.SL2.HasEigenvalues {F : Type u_1} [Field F] (M : Matrix.SpecialLinearGroup (Fin 2) F) (s : F) : Prop

def SimpleGroups.SL2.IsConjToDiag {F : Type u_1} [Field F] (M : Matrix.SpecialLinearGroup (Fin 2) F) (s : F) : Prop

theorem SimpleGroups.sl2_normal_subgroup_contains_all_conj_to_diag {F : Type u_1} [Field F] (N : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) (hN : N.Normal) (s : F) (B : Matrix.SpecialLinearGroup (Fin 2) F) (hB : B ∈ N) (hBdiag : SL2.IsConjToDiag B s) (Q : Matrix.SpecialLinearGroup (Fin 2) F) (hQdiag : SL2.IsConjToDiag Q s) : Q ∈ N

theorem SimpleGroups.sl2_eigenvalues_implies_conj_to_diag {F : Type u_1} [Field F] (s : F) (hs : s ≠ s⁻¹) (M : Matrix.SpecialLinearGroup (Fin 2) F) (hM : SL2.HasEigenvalues M s) : SL2.IsConjToDiag M s

theorem SimpleGroups.sl2_normal_contains_all_with_eigenvalues {F : Type u_1} [Field F] (N : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) (hN : N.Normal) (s : F) (hs : s ≠ s⁻¹) (B : Matrix.SpecialLinearGroup (Fin 2) F) (hB : B ∈ N) (hBeig : SL2.HasEigenvalues B s) (Q : Matrix.SpecialLinearGroup (Fin 2) F) (hQeig : SL2.HasEigenvalues Q s) : Q ∈ N

theorem SimpleGroups.det_exp (n : ℕ) (A : Matrix (Fin n) (Fin n) ℂ) : (NormedSpace.exp A).det = NormedSpace.exp A.trace