Documentation

Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

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
Instances For
    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
    Equations
    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,
    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