elementary symmetric polynomial is not equal to 0

Stream: new members

[Hanting Zhang]

Are there any tools in mathlib that can help with this? This tiny detail is surprising resilient to anything I throw at it.

import ring_theory.polynomial.symmetric

open fintype

namespace mv_polynomial
variables {σ : Type*} [fintype σ] {R : Type*} [comm_semiring R]

instance [nontrivial R] : nontrivial (mv_polynomial σ R) := add_monoid_algebra.nontrivial

lemma esymm_ne_zero (n : ℕ) (h : n ≤ card σ) [nontrivial R] : esymm σ R n ≠ 0 :=
begin
  sorry
end

end mv_polynomial

[Johan Commelin]

@Hanting Zhang Can you prove something about docs#mv_polynomial.degrees of esymm?

[Johan Commelin]

In particular there is docs#mv_polynomial.degrees_add_of_disjoint which might be relevant (although there doesn't seem to be a version for finset.sum yet)

[Johan Commelin]

Basically, I guess it might make sense to first show that the polynomials are homogeneous of degree n, and proceed from there

[Hanting Zhang]

Ah. I think I can build something out of this. Your suggestions sound much better than the plan I had inside my head. :rolling_on_the_floor_laughing: Thanks!