Zulip Chat Archive

Stream: maths

Topic: det_vandermonde_eq_zero

Bart Michels (Jun 10 2022 at 12:47):

I've written two small lemmas about Vandermonde determinants (that I need somewhere else). Is there a branch I can get write access to, or should I create my own?
My github username is bartmichels.

lemma det_vandermonde_eq_zero_iff {R : Type*} [comm_ring R] [is_domain R] {n : ℕ} (v : fin n → R) :
  det (vandermonde v) = 0 ↔ ∃ (i j : fin n), i ≠ j ∧ v i = v j :=
begin
  simp [det_vandermonde v, finset.prod_eq_zero_iff, sub_eq_zero],
  split,
  rintros ⟨i, j, hij⟩,
  exact ⟨j, i, ne_of_gt (hij.left), hij.right⟩,
  rintros ⟨i, j, hij⟩,
  cases lt_or_gt_of_ne hij.left with hilt higt,
  exact ⟨i, j, hilt, by symmetry; exact hij.right⟩,
  exact ⟨j, i, higt, hij.right⟩,
end

lemma det_vandermonde_ne_zero_iff {R : Type*} [comm_ring R] [is_domain R] {n : ℕ} (v : fin n → R) :
  det (vandermonde v) ≠ 0 ↔ function.injective v :=
by simpa [det_vandermonde_eq_zero_iff, not_imp_not]

Also, if you can make the proof of the first one shorter, please do :)

Ruben Van de Velde (Jun 10 2022 at 12:54):

At least, you'll want to use squeeze_simp or simp? on that first line, and put braces { } around the subgoals after split

Damiano Testa (Jun 10 2022 at 12:59):

I'm not sure if this is desirable, but you can "golf" the statement asserting that v is not injective.

Bart Michels (Jun 10 2022 at 13:03):

Right, thanks. I added the braces and indentation for subgoals.

Bart Michels (Jun 10 2022 at 13:19):

Damiano Testa said:

I'm not sure if this is desirable, but you can "golf" the statement asserting that v is not injective.

Certainly desirable, I'll try.

Bart Michels (Jun 10 2022 at 16:11):

I can replace the "not injective" part with a single term (or split and two terms) that's not so horrible, for the most part:

split,
{ exact Exists₂.imp (λ i j h, ⟨ne_of_lt h.left, h.right.symm ⟩) },
{ exact λ h, exists.elim h (λ i h, exists.elim h (λ j h₁, ⟨min i j, max i j,
          min_lt_max.mpr h₁.left, ((fn_min_eq_fn_max_iff v i j).mpr h₁.right).symm ⟩)) }

It would be nice to have an exists₂.elim.
I also didn't find any term-mode ways to wlog assume i ≤ j. Is there anything? Here it's hidden in fn_min_eq_fn_max_iff, which is another lemma (that does not exist yet), to show v n = v m → v (min n m) = v (max n m).