# Zulip Chat Archive

## Stream: maths

### Topic: mv_polynomial questions

#### 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`

.

#### 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

#### Kenny Lau (Mar 28 2020 at 13:48):

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

#### 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?

#### 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

#### 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)

#### 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

#### 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`

#### Mario Carneiro (Mar 28 2020 at 22:25):

`eq_zero_iff`

looks like a version of extensionality

#### Mario Carneiro (Mar 28 2020 at 22:26):

it should just be a rewrite with `ext_iff`

#### Scott Morrison (Mar 29 2020 at 00:32):

I would love to change the behaviour of `by_cases`

to produce `≠`

.

#### Scott Morrison (Mar 29 2020 at 00:32):

I would also love to remove `ne.def`

from the simp set.

#### Mario Carneiro (Mar 29 2020 at 00:34):

removing `ne.def`

would cause similar problems as noted with `gt`

here

#### Scott Morrison (Mar 29 2020 at 00:50):

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

#### Scott Morrison (Mar 29 2020 at 00:51):

(what about reversing the direction of `ne.def`

, and keeping it as a simp lemma?)

#### 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