Determinants

This file provides lemmas about determinants that are not present in Mathlib.

theorem Matrix.isUnit_2x2 (A : Matrix (Fin 2) (Fin 2) Z2) (hA : IsUnit A) : ∃ (f : Fin 2 ≃ Fin 2) (g : Fin 2 ≃ Fin 2), A.submatrix ⇑f ⇑g = 1 ∨ A.submatrix ⇑f ⇑g = !![1, 1; 0, 1]

Lemma 10 (motivates the difference between the definition of 3-sum in our implementation and in Truemper's book).

theorem Matrix.det_eq_zero_of_col_eq_mul_col {Z R : Type} [Fintype Z] [DecidableEq Z] [CommRing R] (A : Matrix Z Z R) (j₀ j₁ : Z) (hjj : j₀ ≠ j₁) (k : R) (hAjj : ∀ (i : Z), A i j₀ = k * A i j₁) : A.det = 0

theorem Matrix.det_eq_zero_of_col_sub_col_eq_col {Z R : Type} [Fintype Z] [DecidableEq Z] [CommRing R] [CommRing R] [IsDomain R] (A : Matrix Z Z R) (j₀ j₁ j₂ : Z) (hAjjj : ((fun (x : Z) => A x j₀) - fun (x : Z) => A x j₁) = fun (x : Z) => A x j₂) : A.det = 0

theorem Matrix.submatrix_det_zero_of_not_injective_cols {Z R : Type} [Fintype Z] [DecidableEq Z] [CommRing R] {X Y : Type} (A : Matrix X Y R) (f : Z → X) {g : Z → Y} (hg : ¬Function.Injective g) : (A.submatrix f g).det = 0

theorem Matrix.submatrix_det_zero_of_not_injective_rows {Z R : Type} [Fintype Z] [DecidableEq Z] [CommRing R] {X Y : Type} (A : Matrix X Y R) {f : Z → X} (g : Z → Y) (hf : ¬Function.Injective f) : (A.submatrix f g).det = 0