Formalizing the product of complex roots

Stream: new members

[Janitha]

Suppose I have a polynomial of degree 4 over the real numbers (I know this polynomial). How do I formalize the statement that the product of the complex roots is p, where p is a real number?

[Aaron Liu]

(P.map Complex.ofRealHom).roots.prod = Complex.ofReal p (this counts multiple roots multiple times)

[Damiano Testa]

There is also docs#Polynomial.prod_roots_eq_coeff_zero_of_monic_of_splits that can be useful.

[Janitha]

example (P  :  ℝ) (f  :  ℝ [X]) (h : (f.map Complex.ofRealHom).roots.prod = Complex.ofReal P) (h'  :  f = /- to fill -/): /-to fill-/ := by

I want to capture the idea that the product of the complex roots of f is P. Is this correct?

[Aaron Liu]

This says,
"Suppose P is a real number, f is a polynomial with real coefficients, the product of the complex roots of f counted by multiplicity is P, and f is equal to /- to fill -/. Then /- to fill -/."

[Janitha]

Thank you! That's what I wanted to say.

[Janitha]

I'm stuck again. I've calculated the roots of my polynomial. Say they are r_1, r_2, r_3, r_4 with r_1, r_2 the only two complex roots . I tried to get

h1 :  r_1.IsRoot f := by sorry

But I got an error :

invalid field 'IsRoot', the environment does not contain 'Real.IsRoot'
  r_1
has type
  ℝ

How do I fix this? My goal is to compute P ', the product of the two complex roots of f`.

[Aaron Liu]

This should be f.IsRoot r_1, or Polynomial.IsRoot f r_1 (they mean the same thing)

[Janitha]

Thank you again!

[Janitha]

@Aaron Liu I had thought complex roots meant non-real roots. How would I modify

example (P  :  ℝ) (f  :  ℝ [X]) (h : (f.map Complex.ofRealHom).roots.prod = Complex.ofReal P) (h'  :  f = /- to fill -/): /-to fill-/ := by

to say that P is the product of non-real roots?

[Aaron Liu]

example (P : ℝ) (f : ℝ[X]) (h : ((f.map Complex.ofRealHom).roots.filter (·.im ≠ 0)).prod = Complex.ofReal P) (h' : f = /- to fill -/) : /-to fill-/ := by

[Janitha]

Could you please tell me what the \. in (\. .im \neq 0) stands for? And can you point me to a reference about these? Thank you!

[Aaron Liu]

From the docs:

A placeholder for an implicit lambda abstraction's variable. The lambda abstraction is scoped to the surrounding parentheses. For example, (· + ·) is equivalent to fun x y => x + y.

[Aaron Liu]

The parser is docs#Lean.Parser.Term.cdot