[Merged by Bors] - feat: port Data.MvPolynomial.Funext

[Parcly-Taxel]

---

[Parcly-Taxel]

If this line is absent, there are timeouts. Should I leave it this way?

[semorrison]

At minimum, needs to have a -- Porting note

[semorrison]

I'm trying to look at this now, but waiting on oleans / cache get! problems.

Two possibilities that I'd be okay with:

1. Leave it in, with a porting note
2. Split out two separate lemmas funext_fin_zero and funext_fin_succ.

[semorrison]

Okay, the answer here is that this proof should never have been in mathlib3 in the first place. There is a lemma that should have been factored out:

theorem eval_eval_finSuccEquiv (f : MvPolynomial (Fin (n + 1)) R) :
    (eval x) (Polynomial.eval q (finSuccEquiv R n f)) = eval (Fin.cons (eval x q) x) f := sorry

private theorem funext_fin {n : ℕ} {p : MvPolynomial (Fin n) R}
    (h : ∀ x : Fin n → R, eval x p = 0) : p = 0 := by
  induction' n with n ih
  · apply (MvPolynomial.isEmptyRingEquiv R (Fin 0)).injective
    rw [RingEquiv.map_zero]
    convert h finZeroElim
  · apply (finSuccEquiv R n).injective
    simp only [AlgEquiv.map_zero]
    refine Polynomial.funext fun q => ?_
    rw [Polynomial.eval_zero]
    apply ih fun x => ?_
    calc _ = _ := eval_eval_finSuccEquiv p
         _ = 0 := h _

eval_eval_finSuccEquiv needs to be proved, and moved to Mathlib.Data.MvPolynomial.Equiv, after eval_eq_eval_mv_eval'.

In @jcommelin's defence, when he wrote this proof in leanprover-community/mathlib#4196 the API in Mathlib.Data.MvPolynomial.Equiv wasn't as developed.

@Parcly-Taxel, do you want to tackle this? (Up to you of course.)

[semorrison]

@Parcly-Taxel, I went down the rabbit hole and proved the theorem. There are some TODOs about things that need to be moved, still.

[Parcly-Taxel]

@semorrison Should we make a mathlib3 PR that moves the theorems to their proper files and rewrites funext_fin accordingly?

[eric-wieser]

I think that would be a great idea, if you're up for it

[semorrison]

I've done this now.

[semorrison]

As I've now written most of this, can someone else please review and merge?

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style