Zulip Chat Archive

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 :=

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: Dec 20 2023 at 11:08 UTC