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

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

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