Matrices with fixed determinant

This file defines the type of matrices with fixed determinant m and proves some basic results about them.

Note: Some of this was done originally in Lean 3 in the kbb (https://github.com/kim-em/kbb/tree/master) repository, so credit to those authors.

def FixedDetMatrix (n : Type u_1) [DecidableEq n] [Fintype n] (R : Type u_2) [CommRing R] (m : R) : Type (max 0 u_1 u_2)

The set of matrices with fixed determinant m.

Equations

• FixedDetMatrix n R m = { A : Matrix n n R // A.det = m }

theorem FixedDetMatrix.ext' (n : Type u_1) [DecidableEq n] [Fintype n] (R : Type u_2) [CommRing R] {m : R} {A : FixedDetMatrix n R m} {B : FixedDetMatrix n R m} (h : ↑A = ↑B) : A = B

Extensionality theorem for FixedDetMatrix with respect to the underlying matrix, not entriwise.

theorem FixedDetMatrix.ext_iff {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommRing R] {m : R} {A : FixedDetMatrix n R m} {B : FixedDetMatrix n R m} : A = B ↔ ∀ (i j : n), ↑A i j = ↑B i j

theorem FixedDetMatrix.ext (n : Type u_1) [DecidableEq n] [Fintype n] (R : Type u_2) [CommRing R] {m : R} {A : FixedDetMatrix n R m} {B : FixedDetMatrix n R m} (h : ∀ (i j : n), ↑A i j = ↑B i j) : A = B

instance FixedDetMatrix.instSMulSpecialLinearGroup (n : Type u_1) [DecidableEq n] [Fintype n] (R : Type u_2) [CommRing R] (m : R) : SMul (Matrix.SpecialLinearGroup n R) (FixedDetMatrix n R m)

Equations

• FixedDetMatrix.instSMulSpecialLinearGroup n R m = { smul := fun (g : Matrix.SpecialLinearGroup n R) (A : FixedDetMatrix n R m) => ⟨↑g * ↑A, ⋯⟩ }

theorem FixedDetMatrix.smul_def (n : Type u_1) [DecidableEq n] [Fintype n] (R : Type u_2) [CommRing R] (m : R) (g : Matrix.SpecialLinearGroup n R) (A : FixedDetMatrix n R m) : g • A = ⟨↑g * ↑A, ⋯⟩

instance FixedDetMatrix.instMulActionSpecialLinearGroup (n : Type u_1) [DecidableEq n] [Fintype n] (R : Type u_2) [CommRing R] (m : R) : MulAction (Matrix.SpecialLinearGroup n R) (FixedDetMatrix n R m)

Equations

• FixedDetMatrix.instMulActionSpecialLinearGroup n R m = MulAction.mk ⋯ ⋯

theorem FixedDetMatrix.smul_coe (n : Type u_1) [DecidableEq n] [Fintype n] (R : Type u_2) [CommRing R] (m : R) (g : Matrix.SpecialLinearGroup n R) (A : FixedDetMatrix n R m) : ↑(g • A) = ↑g * ↑A