# Zulip Chat Archive

## Stream: new members

### Topic: The type of even integers

#### Lars Ericson (Dec 24 2020 at 01:37):

I am working on an exercise "are all even integers an integral domain". In Lean, I think this means I need to create the **type** of even integers as opposed to creating the **set** of even integers, because my sense so far is that sets can't be used in place of types, more or less. So I want to do this to set the problem up, but I am worried that it is not correct:

```
def ℕ_even := {x : ℕ | ∃ y, x = 2 * y}
instance : integral_domain ℕ_even := sorry
```

I will need to make more of these somewhat ad hoc set-types which don't necessarily have any structure, for example "all rational numbers whose denominators are a power of 2".

#### Yury G. Kudryashov (Dec 24 2020 at 01:44):

You can use either `{x : ℕ | ∃ y, x = 2 * y}`

or `{x : ℕ // ∃ y, x = 2 * y}`

. In the former case, it is a `set ℕ`

but it has an automatic coercion to `Type`

. In the latter case, it is already a `Type`

.

#### Mario Carneiro (Dec 24 2020 at 01:44):

you can also use `{n | even n}`

by the way

#### Yury G. Kudryashov (Dec 24 2020 at 01:45):

If you want some instances to be deduced automatically (e.g., `add_comm_monoid`

), then you might want to use docs#add_submonoid.closure like in `add_submonoid.closure {2}`

#### Mario Carneiro (Dec 24 2020 at 01:45):

the easiest way to get the full result by abstract nonsense is to express it as the span of {2}

#### Mario Carneiro (Dec 24 2020 at 01:46):

we should have the theorem that says that you are in the span of a singleton iff you divide the element

#### Lars Ericson (Dec 24 2020 at 01:47):

Thanks I will follow your suggestions. This is the exercise. Some will be integral domains and some won't. The ones that are will fit into the "instance" pattern. For the ones that aren't I guess I have to show an example where an integral domain axiom is violated:

Screenshot-from-2020-12-23-20-44-18.png

#### Yury G. Kudryashov (Dec 24 2020 at 01:47):

Do you mean docs#add_submonoid.closure or docs#subalgebra.span?

#### Mario Carneiro (Dec 24 2020 at 01:48):

certainly (d) and (e) are best expressed as spans

#### Yury G. Kudryashov (Dec 24 2020 at 01:48):

docs#integral_domain says that you need `1`

#### Mario Carneiro (Dec 24 2020 at 01:48):

you could use an `add_submonoid.closure`

but we're after a ring structure here

#### Yury G. Kudryashov (Dec 24 2020 at 01:49):

docs#subalgebra.span pulls in at least all integers

#### Mario Carneiro (Dec 24 2020 at 01:49):

Well in those cases I suppose the theorem is false so it doesn't matter

#### Mario Carneiro (Dec 24 2020 at 01:50):

if you want to prove it's not an integral domain the proof strategy is different

#### Yury G. Kudryashov (Dec 24 2020 at 01:50):

First, you need to define a predicate `is_integral_subdomain`

on a `set R`

provided `[ring R]`

#### Yury G. Kudryashov (Dec 24 2020 at 01:51):

It should say that you have a subring + the natural ring structure on the subtype defines an integral domain.

#### Yury G. Kudryashov (Dec 24 2020 at 01:52):

Otherwise you can't formalize arguments like "this set does not contain 1, so it's not an integral domain".

#### Mario Carneiro (Dec 24 2020 at 01:52):

You don't need the same 1

#### Mario Carneiro (Dec 24 2020 at 01:53):

you can still reason that the set does not contain any idempotent element and hence can't have a 1-alike

#### Mario Carneiro (Dec 24 2020 at 01:55):

do we have a notion of subring that doesn't require that 1 come along? I guess that's a subrng

#### Yury G. Kudryashov (Dec 24 2020 at 01:55):

Yes, the problem is ill-formulated. Each of those sets is an integral domain (w.r.t. some `*`

, `+`

, `0`

, and `1`

) because there exist a countable integral domain. The problem doesn't say what operations/constants must agree with those in `real`

#### Yury G. Kudryashov (Dec 24 2020 at 01:55):

AFAIK, `subrng`

is not in mathlib

#### Mario Carneiro (Dec 24 2020 at 01:56):

it might be nice to have something like that even if we don't have non-unital rings, because I think they come up in banach spaces

#### Mario Carneiro (Dec 24 2020 at 01:57):

you can have two rings which share the same operations but are not in a subring relation because the unit of the subobject is different

Last updated: Dec 20 2023 at 11:08 UTC