formalising def of alg closed fields

Stream: maths

[Kevin Buzzard]

It is a source of some frustration to me that I still often don't know the best way to proceed when defining new concepts in Lean. Proofs I feel like I have learnt a lot of the techniques (tactic/term mode etc). But I found myself on the way back from Pittsburgh wanting alg closed fields, and ended up writing this:

import data.polynomial
import analysis.complex.polynomial -- just a sanity check, probably shouldn't be imported

open polynomial

class algebraically_closed_field (k : Type*) extends discrete_field k :=
(exists_root' : ∀ (f : polynomial k) (hf : 0 < degree f),
   ∃ z : k, is_root f z)

namespace algebraically_closed_field

variables {k : Type*} [algebraically_closed_field k]

def exists_root {f : polynomial k} (hf : 0 < degree f) := ∃ z : k, is_root f z

-- sanity check
noncomputable example : algebraically_closed_field ℂ :=
{exists_root' := λ f hf, complex.exists_root hf,
..complex.discrete_field}

end algebraically_closed_field

def is_algebraically_closed (k : Type*) [discrete_field k] : Prop :=
  ∀ {f : polynomial k} (hf : 0 < degree f), ∃ z : k, is_root f z

-- sanity check
example : is_algebraically_closed ℂ := λ hf, complex.exists_root

Should it be a new class, or just a definition? What should I be doing in order to be able to confidently make this decision myself?

[Patrick Massot]

You can make it a class either way. The question is only whether it should extend discrete_field or take it as a parameter.

[Patrick Massot]

Since it doesn't use more types than discrete_field, Mario's rule is to extend.

[Patrick Massot]

But I guess either way would be fine.

[Kevin Buzzard]

But I guess either way would be fine.

This is exactly the problem! There is so often more than one way to do it and I never know which one to choose.