Matrix whose column sum to zero

Stream: Is there code for X?

[Xavier Roblot]

Let M be a r × (r+1) matrix such that the sum of its column is equal to zero. Then all square matrices obtained by deleting one column of M have the same determinant in absolute value. (This is a well-known results for people that works on the regulator of a number field :wink:) I don't think we have anything like this in the library but we might have something close enough.

Also, I have the feeling that there is probably a better, more general way, of stating the result.

[Johan Commelin]

Hmm, have you already tried stating it in Lean? Because my first naive guess would involve Matrix.reindex and I think it would quickly become quite ugly.

[Xavier Roblot]

I have a statement although I am not sure it is 100% correct (there's a good chance I mixed up rows and columns somewhere):

import Mathlib

open BigOperators Classical

variable {m n : Type*} [Fintype m] [Fintype n]
  {R : Type*} [LinearOrderedCommRing R] (v : n → m → R) (hv : ∑ j, v j = 0)

variable {j₁ j₂ : n} (e₁ : m ≃ {j // j ≠ j₁}) (e₂ : m ≃ {j // j ≠ j₂})

example : |(Matrix.of fun i j ↦ v (e₁ i) j).det| = |(Matrix.of fun i j ↦ v (e₂ i) j).det| := by
  sorry

[Xavier Roblot]

But indeed, it gets messy very rapidly and I want to make sure it is the right way to go before working on it more. (Right now, I am trying to see if I could use docs#Algebra.discr somehow...)

[Johan Commelin]

I think your statement is even relatively clean...

[Eric Wieser]

I think using reindex is still slightly cleaner there, but not by much

[Andrew Yang]

I would first state it as

import Mathlib

open BigOperators Classical

variable {n : ℕ} {R : Type*} [LinearOrderedCommRing R]
  (M : Matrix (Fin (n + 1)) (Fin n) R) (hv : ∑ j, M j = 0)

variable (j₁ j₂ : Fin (n + 1))

example : |(M.submatrix (Fin.succAbove j₁) id).det| = |(M.submatrix (Fin.succAbove j₂) id).det| := by
  sorry

An then generalize to Fintype.

[Xavier Roblot]

Hum, that sounds like a sensible idea...

[Andrew Yang]

And I think the factor is Int.negOnePow (j₁ - j₂) • so it works for arbitrary (comm)rings

[Yakov Pechersky]

Check out docs#Matrix.det_succ_column_zero and the other Laplacian expansion lemmas for references on how submatrix is used

[Johan Commelin]

That's a clean way of stating it!

[Xavier Roblot]

#13475