Prove that a MvPolynomial is symmetric

Stream: new members

[Xitai Jiang]

I had been stuck to this point for a long time. I have that f (x, y, z) = f (y, x, z) = f (x, z, y) for all real numbers x, y, z, and how can I prove f is symmetric? Much thanks to all replies!

import Mathlib
theorem algebra_181 (P : MvPolynomial (Fin 3) ℝ) (h : ∀ x y z : ℝ,
  (MvPolynomial.eval ![x, y, z] P = MvPolynomial.eval ![y, x, z] P ∧ MvPolynomial.eval ![x, y, z] P = MvPolynomial.eval ![x, z, y] P)) : P.IsSymmetric := by
    simp [MvPolynomial.IsSymmetric]
    intro e
    fin_cases e
    simp
    all_goals
    sorry

[Riccardo Brasca]

I think doing it by brute force is going to be a pain. First of all one should prove that it is enough to prove symmetry wrt to a generating set of $S_n$ (this can very well be already in the library), and then you are basically assuming that.

[Philippe Duchon]

For polynomials with real coefficients, one informal proof would go through the fact that coefficients can be recovered by taking derivatives and evaluating at 0; I don't know how difficult it would be to follow this path in Lean.