# Zulip Chat Archive

## Stream: maths

### Topic: formalising def of alg closed fields

#### Kevin Buzzard (Jan 12 2020 at 20:13):

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 (Jan 12 2020 at 20:17):

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 (Jan 12 2020 at 20:18):

Since it doesn't use more types than `discrete_field`

, Mario's rule is to extend.

#### Patrick Massot (Jan 12 2020 at 20:18):

But I guess either way would be fine.

#### Kevin Buzzard (Jan 12 2020 at 20:19):

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.

Last updated: May 14 2021 at 19:21 UTC