theorem Matrix.fin_two_ext {R : Type u_1} [CommSemiring R] {M N : Matrix (Fin 2) (Fin 2) R} (h₀₀ : M 0 0 = N 0 0) (h₀₁ : M 0 1 = N 0 1) (h₁₀ : M 1 0 = N 1 0) (h₁₁ : M 1 1 = N 1 1) : M = N

theorem SpecialLinearGroup.fin_two_ext {R : Type u} [CommRing R] (A B : Matrix.SpecialLinearGroup (Fin 2) R) (h₀₀ : ↑A 0 0 = ↑B 0 0) (h₀₁ : ↑A 0 1 = ↑B 0 1) (h₁₀ : ↑A 1 0 = ↑B 1 0) (h₁₁ : ↑A 1 1 = ↑B 1 1) : A = B

def SpecialMatrices.s {F : Type u} [Field F] (σ : F) : Matrix.SpecialLinearGroup (Fin 2) F

Equations

• SpecialMatrices.s σ = ⟨!![1, 0; σ, 1], ⋯⟩

@[simp]

theorem SpecialMatrices.s_zero_eq_one {F : Type u} [Field F] : s 0 = 1

theorem SpecialMatrices.s_eq_s_iff {F : Type u} [Field F] (σ μ : F) : s σ = s μ ↔ σ = μ

theorem SpecialMatrices.s_eq_one_iff {F : Type u} [Field F] (σ : F) : s σ = 1 ↔ σ = 0

@[simp]

theorem SpecialMatrices.s_inv {F : Type u} [Field F] (σ : F) : (s σ)⁻¹ = s (-σ)

@[simp]

theorem SpecialMatrices.inv_neg_t_eq {F : Type u} [Field F] (σ : F) : (-s σ)⁻¹ = -s (-σ)

@[simp]

theorem SpecialMatrices.s_mul_s_eq_s_add {F : Type u} [Field F] (σ μ : F) : s σ * s μ = s (σ + μ)

@[simp]

theorem SpecialMatrices.s_pow_eq_s_mul {F : Type u} [Field F] (σ : F) (n : ℕ) : s σ ^ n = s (n • σ)

theorem SpecialMatrices.order_t_eq_char {F : Type u} [Field F] {p : ℕ} [hp : Fact (Nat.Prime p)] [hC : CharP F p] (σ : F) (hσ : σ ≠ 0) : orderOf (s σ) = p

def SpecialMatrices.d {F : Type u_1} [Field F] (δ : Fˣ) : Matrix.SpecialLinearGroup (Fin 2) F

Equations

• SpecialMatrices.d δ = ⟨!![↑δ, 0; 0, (↑δ)⁻¹], ⋯⟩

@[simp]

theorem SpecialMatrices.inv_d_eq_d_inv {F : Type u} [Field F] (δ : Fˣ) : (d δ)⁻¹ = d δ⁻¹

theorem SpecialMatrices.d_eq_inv_d_inv {F : Type u} [Field F] (δ : Fˣ) : d δ = (d δ⁻¹)⁻¹

theorem SpecialMatrices.d_eq_diagonal {F : Type u} [Field F] (δ : Fˣ) : ↑(d δ) = Matrix.diagonal fun (i : Fin 2) => if ↑i = 0 then ↑δ else δ.inv

@[simp]

theorem SpecialMatrices.d_one_eq_one {F : Type u} [Field F] : d 1 = 1

@[simp]

theorem SpecialMatrices.d_neg_one_eq_neg_one {F : Type u} [Field F] : d (-1) = -1

@[simp]

theorem SpecialMatrices.neg_d_eq_d_neg {F : Type u} [Field F] (δ : Fˣ) : -d δ = d (-δ)

theorem SpecialMatrices.d_coe_eq {F : Type u} [Field F] {δ : Fˣ} : ↑(d δ) = !![↑δ, 0; 0, (↑δ)⁻¹]

theorem SpecialMatrices.d_0_0_is_unit {F : Type u} [Field F] (δ : Fˣ) : IsUnit (↑(d δ) 0 0)

@[simp]

theorem SpecialMatrices.d_mul_d_eq_d_mul {F : Type u} [Field F] (δ ρ : Fˣ) : d δ * d ρ = d (δ * ρ)

theorem SpecialMatrices.s_eq_d_iff {F : Type u} [Field F] {δ : Fˣ} {σ : F} : d δ = s σ ↔ δ = 1 ∧ σ = 0

def SpecialMatrices.w {F : Type u_1} [Field F] : Matrix.SpecialLinearGroup (Fin 2) F

Equations

• SpecialMatrices.w = ⟨!![0, 1; -1, 0], ⋯⟩

@[simp]

theorem SpecialMatrices.w_inv {F : Type u_1} [Field F] : w⁻¹ = -w

theorem SpecialMatrices.w_mul_w_eq_neg_one {F : Type u} [Field F] : w * w = -1

def SpecialMatrices.ds {F : Type u} [Field F] (δ : Fˣ) (σ : F) : Matrix.SpecialLinearGroup (Fin 2) F

Equations

• SpecialMatrices.ds δ σ = ⟨!![↑δ, 0; σ * ↑δ⁻¹, (↑δ)⁻¹], ⋯⟩

theorem SpecialMatrices.d_mul_s_mul_d_inv_eq_s {F : Type u} [Field F] (δ : Fˣ) (σ : F) : d δ * s σ * (d δ)⁻¹ = s (σ * ↑δ⁻¹ * ↑δ⁻¹)

def SpecialMatrices.dw {F : Type u} [Field F] (δ : Fˣ) : Matrix.SpecialLinearGroup (Fin 2) F

Equations

• SpecialMatrices.dw δ = ⟨!![0, ↑δ; -↑δ⁻¹, 0], ⋯⟩

theorem SpecialMatrices.d_mul_s_eq_ds {F : Type u} [Field F] (δ : Fˣ) (σ : F) : d δ * s σ = ds δ σ

theorem SpecialMatrices.d_mul_w_eq_dw {F : Type u} [Field F] (δ : Fˣ) : d δ * w = dw δ

@[simp]

theorem SpecialMatrices.inv_of_d_mul_w {F : Type u} [Field F] (δ : Fˣ) : (d δ * w)⁻¹ = d (-δ) * w

theorem SpecialMatrices.w_mul_d_mul_inv_w_eq_inv_d {F : Type u} [Field F] (δ : Fˣ) : w * d δ * w⁻¹ = (d δ)⁻¹

@[simp]

theorem SpecialMatrices.w_mul_d_eq_d_inv_w {F : Type u} [Field F] (δ : Fˣ) : w * d δ = (d δ)⁻¹ * w

@[simp]

theorem SpecialMatrices.neg_d_mul_w {F : Type u} [Field F] (δ : Fˣ) : -(d δ * w) = d (-δ) * w