## Stream: maths

### Topic: Ideal

#### Ashvni Narayanan (Jun 21 2020 at 11:43):

Are ideals in Lean defined only for commutative rings?

Yes :oh_no:

(deleted)

#### Ashvni Narayanan (Jun 21 2020 at 11:49):

Chris Hughes said:

Yes :oh_no:

Ahh alright.

#### Ashvni Narayanan (Jun 21 2020 at 12:07):

I am trying to prove that the valuation ring corresponding to a discrete valuation field is a discrete valuation ring(defined to be a pid with a unique nonzero prime ideal).

lemma has_discrete_valuation (K:Type*) [field K] [discrete_valuation_field K] (S : Type*) (h : S = {x : K | val(x) ≥ 0}) : discrete_valuation_ring S :=
begin
have P := {x : K | val(x) > 0},
have f : principal_ideal_domain S,
sorry,
have P : ideal S,
sorry,
end


The 3rd last line of the proof gives me an error:

failed to synthesize type class instance for
K : Type u_1,
_inst_2 : field K,
_inst_3 : discrete_valuation_field K,
S : Type u_1,
h : S = ↥{x : K | val x ≥ 0},
P : set K,
f : principal_ideal_domain S
⊢ comm_ring S


I don't know how to input the info that S is commutative. Any help is appreciated. Thank you!

#### Reid Barton (Jun 21 2020 at 12:17):

What did you already prove about {x : K | val(x) ≥ 0}?

#### Kevin Buzzard (Jun 21 2020 at 12:17):

comm_ring S is in some sense not a good goal, because it's not (at least as far as Lean is concerned) a true/false statement.

#### Reid Barton (Jun 21 2020 at 12:18):

This setup with h : S = {x : K | val(x) ≥ 0} looks awkward. Better define def valuation_ring (K:Type*) [field K] [discrete_valuation_field K] := {x : K | val(x) ≥ 0} and then write a bunch of instances about it.

#### Kevin Buzzard (Jun 21 2020 at 12:19):

Lean likes things best when they're broken up into coherent chunks which are as small as possible, so rather than launching straight into a proof that the valuation ring is a DVR, you want to first prove simpler things about it, like Reid is hinting. Ten small lemmas is better than one big lemma with lots of sublemmas.

Last updated: May 12 2021 at 08:14 UTC