## Stream: new members

### Topic: elementary symmetric polynomial is not equal to 0

#### Hanting Zhang (Mar 15 2021 at 03:34):

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 (Mar 15 2021 at 03:51):

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

#### Johan Commelin (Mar 15 2021 at 03:52):

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 (Mar 15 2021 at 03:53):

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

#### Hanting Zhang (Mar 15 2021 at 04:28):

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!

Last updated: May 11 2021 at 22:14 UTC