computing degrees of polynomials

Stream: maths

[Kevin Buzzard]

I remember there was some discussion about this a while back but I can't remember the conclusion or find the discussion. @Damiano Testa were you involved? I was just showcasing the fact that $\mathbb{C}$ was algebraically closed and came unstuck:

import analysis.complex.polynomial -- import proof of fundamental theorem of algebra

open_locale polynomial -- notation for polynomials

open polynomial -- so I can write `X` and not `polynomial.X`

noncomputable theory -- we are not supplying algorithms for being able
-- to compute what is about to happen

def f : ℂ[X] := X^5 + X + 37 -- a random polynomial

theorem f_has_a_root : ∃ (z : ℂ), f.is_root z :=
begin
  apply complex.exists_root, -- the fundamental theorem of algebra
  -- ⊢ 0 < f.degree -- gaargh
  sorry
end

A sticking plaster would be to try have foo : f.eval 0 ≠ f.eval 1 := by norm_num [f], as the next line and then invoke a library lemma which I couldn't find saying that if f evaluates to two different things then it can't be constant. But I would rather that norm_num proved that the degree was 5 (perhaps in Lean 4?)

[Damiano Testa]

Kevin, the tactic is in #15691, but I was not going to push for it to get into mathlib, until I felt confident that I could also port it to Lean4. I have been learning some Lean4 during the holidays and may have some time in the coming weeks to help with the port.

[Damiano Testa]

I am now at a computer. On that branch, branch#adomani_compute_degree_take_two, this is valid proof:

theorem f_has_a_root : ∃ (z : ℂ), f.is_root z :=
begin
  apply complex.exists_root, -- the fundamental theorem of algebra
  refine lt_of_lt_of_eq (with_bot.coe_lt_coe.mpr (ne_zero.pos 5)) _,
  symmetry,  -- currently, `compute_degree` wants the polynomial on the left and the degree on the right
  unfold f,  -- also, the tactic does not see through the definition of `f` and treats `f` as a generic polynomial
  compute_degree,  -- now this works
end