# Zulip Chat Archive

## Stream: maths

### Topic: Ideal

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

Are ideals in Lean defined only for commutative rings?

#### Chris Hughes (Jun 21 2020 at 11:47):

Yes :oh_no:

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

(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 `instance`

s 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