Nonsingular minors: proof internals

Proofs behind Complexitylib.Algebraic.LinearAlgebra.NonsingularMinor.

• Dominance. In ∑ ±2^{E x} with pairwise distinct exponents, every term other than the one with the least exponent E₀ is divisible by 2^{E₀ + 1}, while that term is not, so the sum is nonzero.
• Leibniz expansion. If every nonzero entry of an integer matrix is ±2^{2^{L i j}}, then a permutation whose diagonal avoids the zero entries contributes ±2^{E σ} to the determinant, where E σ = ∑_j 2^{L (σ j) j}. If L is injective on the nonzero entries, E σ is the binary number whose set bits are the labels used by σ; these labels determine the pairs (σ j, j), hence σ, so the exponents are pairwise distinct and dominance applies. Over a ring of characteristic zero the matrix is the image of such an integer matrix.
• Block-diagonal minors. A minor that is block diagonal with nonsingular blocks is the Matrix.blockDiagonal of its blocks, so its determinant is their product.

theorem Algebraic.NonsingularMinor.Internal.sum_mul_two_pow_ne_zero {κ : Type u_1} {s : Finset κ} (hs : s.Nonempty) {ε : κ → ℤ} (hε : ∀ x ∈ s, IsUnit (ε x)) {E : κ → ℕ} (hE : Set.InjOn E ↑s) : ∑ x ∈ s, ε x * 2 ^ E x ≠ 0

Dominance. A nonempty sum ∑ ε x * 2 ^ E x with unit coefficients ε x = ±1 and pairwise distinct exponents E x is nonzero.

theorem Algebraic.NonsingularMinor.Internal.det_ne_zero_of_two_pow_two_pow_int {ι : Type u_1} [Fintype ι] [DecidableEq ι] (M : Matrix ι ι ℤ) (L : ι → ι → ℕ) (hM : ∀ (i j : ι), M i j ≠ 0 → M i j = 2 ^ 2 ^ L i j ∨ M i j = -2 ^ 2 ^ L i j) (hL : ∀ (i j i' j' : ι), M i j ≠ 0 → M i' j' ≠ 0 → L i j = L i' j' → i = i' ∧ j = j') (σ₀ : Equiv.Perm ι) (hσ₀ : ∀ (j : ι), M (σ₀ j) j ≠ 0) : M.det ≠ 0

The Leibniz-expansion argument over ℤ.

theorem Algebraic.NonsingularMinor.Internal.det_ne_zero_of_two_pow_two_pow {R : Type u_1} [CommRing R] [CharZero R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (M : Matrix ι ι R) (L : ι → ι → ℕ) (hM : ∀ (i j : ι), M i j ≠ 0 → M i j = 2 ^ 2 ^ L i j ∨ M i j = -2 ^ 2 ^ L i j) (hL : ∀ (i j i' j' : ι), M i j ≠ 0 → M i' j' ≠ 0 → L i j = L i' j' → i = i' ∧ j = j') (σ₀ : Equiv.Perm ι) (hσ₀ : ∀ (j : ι), M (σ₀ j) j ≠ 0) : M.det ≠ 0

The Leibniz-expansion argument over a commutative ring of characteristic zero: the matrix is the image of an integer matrix with the same zero pattern.

theorem Algebraic.NonsingularMinor.Internal.card_mul_card_le_rank_of_det_blocks_ne_zero {K : Type u_1} [Field K] {m : Type u_2} {n : Type u_3} [Fintype n] {ι : Type u_4} {β : Type u_5} [Fintype ι] [DecidableEq ι] [Fintype β] [DecidableEq β] (A : Matrix m n K) (f : ι → β → m) (g : ι → β → n) (hoff : ∀ (i i' : ι) (b b' : β), b ≠ b' → A (f i b) (g i' b') = 0) (hdet : ∀ (b : β), (A.submatrix (fun (x : ι) => f x b) fun (x : ι) => g x b).det ≠ 0) : Fintype.card ι * Fintype.card β ≤ A.rank

A minor that is block diagonal with nonsingular square blocks has nonzero determinant, so its size is at most the rank.