Zulip Chat Archive

Stream: maths

Topic: mv_polynomial questions


view this post on Zulip Kevin Buzzard (Mar 28 2020 at 13:34):

@Shing Tak Lam has been thinking about multivariate polynomials and gave me these three puzzles:

lemma single_eq_C_mul_X (s : S) (a : R) (n : ): monomial (single s n) a = C a * (X s)^n := sorry
lemma erase_single (var : S) (n : ): (erase var (single var n)) = 0 := sorry
lemma erase_single_ne (v1 v2 : S) (n : ) (hv : v1  v2): (erase v1 (single v2 n)) = single v2 n := sorry

Independently, I was wondering whether we have the multivariable polynomial analogue of the statement that a polynomial p equals the sum of coeff p m * X ^m.

view this post on Zulip Johan Commelin (Mar 28 2020 at 13:46):

Re the independent question: I think we only have if for single variable polynomials: https://github.com/leanprover-community/mathlib/search?q=as_sum&unscoped_q=as_sum

view this post on Zulip Kenny Lau (Mar 28 2020 at 13:48):

wait... how do you search on github??

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 13:48):

lemma finsupp.eq_zero_iff {α : Type*} {β : Type*} [has_zero β] (f : α  β) :
  f = 0   x : α, f x = 0 :=
begin
  split,
  { intro hf,
    rw hf,
    intro x,
    refl,
  },
  { intro h,
    ext x,
    exact h x
  }
end

open_locale classical

lemma erase_single (var : S) (n : ): (erase var (single var n)) = 0 :=
begin
  rw finsupp.eq_zero_iff,
  intro x,
  by_cases hx : x = var,
  { rw hx,
    apply erase_same,
  },
  { rw erase_ne hx,
    apply single_eq_of_ne,
    symmetry, assumption
  }
end

I don't know my way around finsupp. Am I making a mountain out of a molehill?

view this post on Zulip Jason KY. (Mar 28 2020 at 13:56):

Kenny Lau said:

wait... how do you search on github??

https://help.github.com/en/github/searching-for-information-on-github/about-searching-on-github

view this post on Zulip Marc Huisinga (Mar 28 2020 at 14:01):

Kenny Lau said:

wait... how do you search on github??

often with plenty of pain because there's still no way to do exact string searches (it's in the beta for some repos, though)

view this post on Zulip Kenny Lau (Mar 28 2020 at 14:03):

import data.mv_polynomial

open finsupp mv_polynomial

universes u v

variables {R : Type u} {S : Type v} [comm_ring R]

lemma single_eq_C_mul_X (s : S) (a : R) (n : ): monomial (single s n) a = C a * (X s)^n :=
by rw [ zero_add (single s n), monomial_add_single, C]

lemma erase_single (var : S) (n : ): (erase var (single var n)) = 0 :=
begin
  ext s, classical, by_cases hs : s = var,
  { rw [hs, erase_same], refl },
  { rw [erase_ne hs], exact single_eq_of_ne (ne.symm hs) }
end

lemma erase_single_ne (v1 v2 : S) (n : ) (hv : v1  v2): (erase v1 (single v2 n)) = single v2 n :=
begin
  ext s, classical, by_cases hs : s = v1,
  { rw [hs, erase_same, single_eq_of_ne (hv.symm)] },
  { rw [erase_ne hs] }
end

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 14:05):

Nice, thanks Kenny. I thought it was a bit annoying that by_cases gave as a case ¬s = var. Would we rather have s ≠ var? Then you can do hs.symm instead of ne.symm hs

view this post on Zulip Mario Carneiro (Mar 28 2020 at 22:25):

eq_zero_iff looks like a version of extensionality

view this post on Zulip Mario Carneiro (Mar 28 2020 at 22:26):

it should just be a rewrite with ext_iff

view this post on Zulip Scott Morrison (Mar 29 2020 at 00:32):

I would love to change the behaviour of by_cases to produce .

view this post on Zulip Scott Morrison (Mar 29 2020 at 00:32):

I would also love to remove ne.def from the simp set.

view this post on Zulip Mario Carneiro (Mar 29 2020 at 00:34):

removing ne.def would cause similar problems as noted with gt here

view this post on Zulip Scott Morrison (Mar 29 2020 at 00:50):

hmm, okay, I guess I don't understand.

view this post on Zulip Scott Morrison (Mar 29 2020 at 00:51):

(what about reversing the direction of ne.def, and keeping it as a simp lemma?)

view this post on Zulip Chris Hughes (Mar 29 2020 at 00:52):

I'd like to make ne notation. I think the only lemma about ne is ne.symm, so it's no great loss.


Last updated: May 14 2021 at 18:28 UTC