Vieta's formulas of polynomials

Stream: Is there code for X?

[Jiang Jiedong]

Are Vieta's formulas in mathlib?

What I really need is the following application: Let $f$ be the minimal polynomial of $x$ over $K$, then the constant term $a_0$ of $f$ is

$$(-1)^n * \prod_{\sigma \in \text{Gal}(K(f)/K) } \sigma (x)$$

It basically boils down to two theorems,

1. Vieta's formula. $a_0 = \prod_{\alpha \text{ is a root of } f } \alpha$. For this, I find Polynomial.C_leadingCoeff_mul_prod_multiset_X_sub_C but it seems a little bit overkilling. Is there a more direct theorem?
2. roots are acted by the Galois group transitively and faithfully, i.e. $\{ \text{root of } f \} = \{ \sigma(x) | \sigma \in \text{Gal}(K(f)/K) \}$. For this, I didn't find a suitable theorem in mathlib.

Thank you for any possible suggestions!

[Riccardo Brasca]

I am not in front of a laptop, but that result is more or less in mathlib. If I remember correctly there is something very similar stated using the norm.

[Riccardo Brasca]

I would have a look in the file about Algebra.norm.

[Jiang Jiedong]

Riccardo Brasca said:

I would have a look in the file about Algebra.norm.

Thank you very much! I found Algebra.norm_eq_prod_automorphisms and Algebra.PowerBasis.norm_gen_eq_coeff_zero_minpoly

[Jiang Jiedong]

I'll look into this PowerBasis more to figure out how to use the second theorem.

[Junyan Xu]

There are docs#AdjoinRoot.powerBasis, docs#IntermediateField.adjoinRootEquivAdjoin