polynomials12

Stream: mathlib4

[BANGJI HU]

i just prove the root of this polynomials how do use "polinomials root"

import Mathlib
open Polynomial Complex BigOperators

noncomputable def P : Polynomial ℝ :=
  C (2 : ℝ) * X^5 + C (-9 : ℝ) * X^4 + C (16 : ℝ) * X^3 + C (-14 : ℝ) * X^2 + C (14 : ℝ) * X + C (-5 : ℝ)

-- Prove that 1/2 is a root of P in ℝ
example : eval (1/2 : ℝ) P = 0 := by
  simp [P, eval_add, eval_sub, eval_mul, eval_pow, eval_C, eval_X]
  norm_num
theorem root_half_is_in_real_roots : (1/2 : ℝ) ∈ P.roots := by
sorry

[Jireh Loreaux]

You'll want to make your first example a lemma so that you can use it in the proof of the theorem. As for the theorem, rw [mem_roots'] will tell you that you need to prove in addition to the example, that P is not zero. I suggest doing this by first showing the natDegree is 5 (using the tacticcompute_degree!), and then using the lemma docs#Polynomial.ne_zero_of_natDegree_gt.

[Jireh Loreaux]

I suggest doing this on your own, but if you're having trouble:

import Mathlib
open Polynomial Complex BigOperators

noncomputable def P : Polynomial ℝ :=
  C (2 : ℝ) * X^5 + C (-9 : ℝ) * X^4 + C (16 : ℝ) * X^3 + C (-14 : ℝ) * X^2 + C (14 : ℝ) * X + C (-5 : ℝ)

-- Prove that 1/2 is a root of P in ℝ
lemma foo : eval (1/2 : ℝ) P = 0 := by
  simp [P, eval_add, eval_sub, eval_mul, eval_pow, eval_C, eval_X]
  norm_num

theorem root_half_is_in_real_roots : (1/2 : ℝ) ∈ P.roots := by
  rw [mem_roots']
  refine ⟨?_, foo⟩
  have : P.natDegree = 5 := by simp [P]; compute_degree!
  exact P.ne_zero_of_natDegree_gt (show 0 < P.natDegree by simp [this])

[BANGJI HU]

i try to prove that i is also a root but the type mismatch

import Mathlib
open Polynomial Complex BigOperators

noncomputable def P : Polynomial ℝ :=
  C (2 : ℝ) * X^5 + C (-9 : ℝ) * X^4 + C (16 : ℝ) * X^3 + C (-14 : ℝ) * X^2 + C (14 : ℝ) * X + C (-5 : ℝ)




theorem root_half_is_in_real_roots :  P.IsRoot (1/2 : ℝ) := by
  -- Goal: IsRoot P (1 / 2) ∧ P ≠ 0
  rw [IsRoot.def]          -- Goal: eval (1 / 2) P = 0 ∧ P ≠ 0
  simp only [P, eval_add, eval_sub, eval_mul, eval_pow, eval_C, eval_X]
  -- Perform the numerical calculation
  norm_num

theorem root_i_is_in_complex_roots_concise : P.IsRoot ( I : ℂ) := by

[Kevin Buzzard]

That's because it's a type mismatch! P has type Polynomial ℝ. Look at the type of docs#Polynomial.IsRoot .