@[simp]

theorem SpecialLinearGroup.coe_coe {F : Type u} [Field F] {n : ℕ} {S : Matrix.SpecialLinearGroup (Fin n) F} : ↑(Matrix.SpecialLinearGroup.toGL S) = ↑S

@[simp]

theorem GeneralLinearGroup.coe_mk' {R : Type u_1} [CommRing R] {M : Matrix (Fin 2) (Fin 2) R} (hM : Invertible M.det) : ↑(Matrix.GeneralLinearGroup.mk' M hM) = M

@[simp]

theorem GeneralLinearGroup.coe_mk'_inv {R : Type u_1} [CommRing R] {M : Matrix (Fin 2) (Fin 2) R} {hM : Invertible M.det} : ↑(Matrix.GeneralLinearGroup.mk' M hM)⁻¹ = M⁻¹

theorem GL_eq_iff_Matrix_eq {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {A B : GL n R} (h : ↑A = ↑B) : A = B

theorem det_GL_coe_is_unit {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (G : GL n R) : IsUnit (↑G).det

theorem associated_of_dvd_mul_irreducibles {k : Type u_1} [Field k] {q p₁ p₂ : Polynomial k} (hp₁ : Irreducible p₁) (hp₂ : Irreducible p₂) (hpq : q ∣ p₁ * p₂) : Associated q 1 ∨ Associated q p₁ ∨ Associated q p₂ ∨ Associated q (p₁ * p₂)

theorem minpoly_eq_X_sub_C_implies_matrix_is_diagonal {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] [NoZeroDivisors R] {M : Matrix n n R} {a : R} (hM : minpoly R M = Polynomial.X - Polynomial.C a) : M = Matrix.diagonal fun (x : n) => a

theorem lower_triangular_iff_top_right_entry_eq_zero {F : Type u} [Field F] {M : Matrix (Fin 2) (Fin 2) F} : (∃ (a : F) (c : F) (d : F), !![a, 0; c, d] = M) ↔ M 0 1 = 0

theorem upper_triangular_iff_bottom_left_entry_eq_zero {F : Type u} [Field F] {M : Matrix (Fin 2) (Fin 2) F} : (∃ (a : F) (b : F) (d : F), !![a, b; 0, d] = M) ↔ M 1 0 = 0

theorem det_eq_mul_diag_of_upper_triangular {F : Type u} [Field F] (S : Matrix.SpecialLinearGroup (Fin 2) F) (hγ : ↑S 1 0 = 0) : ↑S 0 0 * ↑S 1 1 = 1

theorem det_eq_mul_diag_of_lower_triangular {F : Type u} [Field F] (S : Matrix.SpecialLinearGroup (Fin 2) F) (hβ : ↑S 0 1 = 0) : ↑S 0 0 * ↑S 1 1 = 1

theorem SpecialLinearGroup.fin_two_diagonal_iff {F : Type u} [Field F] (x : Matrix.SpecialLinearGroup (Fin 2) F) : ↑x 0 1 = 0 ∧ ↑x 1 0 = 0 ↔ ∃ (δ : Fˣ), SpecialMatrices.d δ = x

theorem SpecialLinearGroup.fin_two_antidiagonal_iff {F : Type u} [Field F] (x : Matrix.SpecialLinearGroup (Fin 2) F) : ↑x 0 0 = 0 ∧ ↑x 1 1 = 0 ↔ ∃ (δ : Fˣ), SpecialMatrices.d δ * SpecialMatrices.w = x

theorem SpecialLinearGroup.fin_two_shear_iff {F : Type u} [Field F] (S : Matrix.SpecialLinearGroup (Fin 2) F) : ↑S 0 0 = ↑S 1 1 ∧ ↑S 0 1 = 0 ↔ (∃ (σ : F), SpecialMatrices.s σ = S) ∨ ∃ (σ : F), -SpecialMatrices.s σ = S

theorem isConj_upper_triangular_iff {F : Type u} [Field F] [DecidableEq F] [IsAlgClosed F] {M : Matrix (Fin 2) (Fin 2) F} : (∃ (a : F) (b : F) (d : F) (C : Matrix.SpecialLinearGroup (Fin 2) F), ↑C * M * ↑C⁻¹ = !![a, b; 0, d]) ↔ ∃ (c : Matrix.SpecialLinearGroup (Fin 2) F), (↑c * M * ↑c⁻¹) 1 0 = 0

@[simp]

theorem Matrix.special_inv_eq {F : Type u} [Field F] {x : F} : !![1, 0; x, 1]⁻¹ = !![1, 0; -x, 1]

theorem exists_root_of_special_poly {F : Type u} [Field F] [IsAlgClosed F] (a b c d : F) (hb : b ≠ 0) : ∃ (x : F), -b * x * x + (a - d) * x + c = 0

theorem Matrix.conj_s_eq {F : Type u} [Field F] {x a b c d : F} : ↑(SpecialMatrices.s x) * !![a, b; c, d] * ↑(SpecialMatrices.s (-x)) = !![-b * x + a, b; -b * x * x + (a - d) * x + c, b * x + d]

def SpecialLinearGroup.mk' {F : Type u} [Field F] {n : ℕ} (M : Matrix (Fin n) (Fin n) F) (h : M.det = 1) : Matrix.SpecialLinearGroup (Fin n) F

Equations

• SpecialLinearGroup.mk' M h = ⟨M, h⟩

theorem isTriangularizable_of_algClosed {F : Type u} [Field F] [DecidableEq F] [IsAlgClosed F] (M : Matrix (Fin 2) (Fin 2) F) : ∃ (a : F) (b : F) (d : F) (C : Matrix.SpecialLinearGroup (Fin 2) F), ↑C * M * ↑C⁻¹ = !![a, b; 0, d]

theorem upper_triangular_isConj_diagonal_of_nonzero_det {F : Type u} [Field F] [DecidableEq F] {a b d : F} (had : a - d ≠ 0) : ∃ (C : Matrix.SpecialLinearGroup (Fin 2) F), ↑C * !![a, b; 0, d] * ↑C⁻¹ = !![a, 0; 0, d]

theorem upper_triangular_isConj_jordan {F : Type u} [Field F] {a b : F} (hb : b ≠ 0) : IsConj !![a, b; 0, a] !![a, 1; 0, a]

theorem lower_triangular_isConj_upper_triangular {F : Type u} [Field F] {a b : F} : ∃ (C : Matrix.SpecialLinearGroup (Fin 2) F), ↑C * !![a, 0; -b, a] * ↑C⁻¹ = !![a, b; 0, a]

theorem mul_left_eq_mul_right_iff {α : Type u_1} [Monoid α] {N M : α} (c : αˣ) : ↑c * M = N * ↑c ↔ M = ↑c⁻¹ * N * ↑c

theorem det_eq_det_IsConj {R : Type u} [CommRing R] {n : ℕ} {M N : Matrix (Fin n) (Fin n) R} (h : IsConj N M) : N.det = M.det

theorem SpecialLinearGroup.eq_of {F : Type u} [Field F] {S L : Matrix.SpecialLinearGroup (Fin 2) F} (h : ↑S = ↑L) : S = L

theorem IsConj_coe {F : Type u} [Field F] {M N : Matrix (Fin 2) (Fin 2) F} (hM : M.det = 1) (hN : N.det = 1) (h : ∃ (C : Matrix.SpecialLinearGroup (Fin 2) F), ↑C * M * ↑C⁻¹ = N) : ∃ (C : Matrix.SpecialLinearGroup (Fin 2) F), C * ⟨M, hM⟩ * C⁻¹ = ⟨N, hN⟩

theorem SL2_IsConj_d_or_IsConj_s_or_IsConj_neg_s {F : Type u} [Field F] [DecidableEq F] [IsAlgClosed F] (S : Matrix.SpecialLinearGroup (Fin 2) F) : (∃ (δ : Fˣ), IsConj (SpecialMatrices.d δ) S) ∨ (∃ (σ : F), IsConj (SpecialMatrices.s σ) S) ∨ ∃ (σ : F), IsConj (-SpecialMatrices.s σ) S