Zulip Chat Archive

Stream: new members

Topic: elementary symmetric polynomial is not equal to 0


view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 15 2021 at 03:51):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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