# Zulip Chat Archive

## Stream: new members

### Topic: int or nat

#### Tianchen Zhao (Apr 05 2021 at 14:45):

Hi all! I encounter this problem trying to replicate this proof in lean (figure 1). I don't know whether to make x y a b to be integers or natural numbers. If they are nat, usually I can stuck on some tedious calculations especially involving subtraction (I guess it's because subtraction is defined differently e.g. 0 - 1 = 0). You can also check figure 2 where I give some examples that library_search cannot solve conjectures about nat but work in int. However, if I make them int, I'll need to combine nat and int using ↑, e.g. ↑q = x^2 + y^2 instead of q = x^2 + y^2 and it takes a lot of work to convert between int and nat.

Are there any suggestions? Thank you!

oringinal-proof.PNG

int-vs-nat.PNG

#### Kevin Buzzard (Apr 05 2021 at 14:46):

I would work with `int`

all the time, because whilst this is a theorem about naturals there is a lot of subtraction going on.

#### Kevin Buzzard (Apr 05 2021 at 14:48):

I would just use ints for everything -- then you don't even have up-arrows.

#### Kevin Buzzard (Apr 05 2021 at 14:49):

As for the not working stuff -- the second example is not true (try `slim_check`

and see if it finds a counterexample) and the first example could perhaps be solved by `omega`

, but honestly I would avoid naturals.

#### Eric Rodriguez (Apr 05 2021 at 15:05):

woah first time I see `slim_check`

, that's really cool

#### Ruben Van de Velde (Apr 05 2021 at 16:44):

If you get stuck, feel free to check https://github.com/Ruben-VandeVelde/flt/blob/tmp/src/cox.lean for my proof

#### Tianchen Zhao (Apr 05 2021 at 17:27):

(deleted)

#### Tianchen Zhao (Apr 05 2021 at 17:28):

Kevin Buzzard said:

I would just use ints for everything -- then you don't even have up-arrows.

I see. I will stick to int later on. Thanks!

#### Tianchen Zhao (Apr 05 2021 at 17:30):

Ruben Van de Velde said:

If you get stuck, feel free to check https://github.com/Ruben-VandeVelde/flt/blob/tmp/src/cox.lean for my proof

Oh that's fantastic! Thank you!

#### Tianchen Zhao (Apr 12 2021 at 11:02):

Kevin Buzzard said:

I would just use ints for everything -- then you don't even have up-arrows.

By the way, there is no defintions for prime in int. To avoid nat, I've seen a lot of works importing field_theory.finite.basic to use the definition of prime. Is that the right thing to do?

#### Ruben Van de Velde (Apr 12 2021 at 11:11):

Not sure why you'd go through `field_theory.finite.basic`

, though it probably works fine. Importing `algebra.associated`

should be sufficient

#### Ruben Van de Velde (Apr 12 2021 at 11:11):

`ring_theory.int.basic`

is probably also useful

#### Tianchen Zhao (Apr 12 2021 at 13:04):

Ruben Van de Velde said:

Not sure why you'd go through

`field_theory.finite.basic`

, though it probably works fine. Importing`algebra.associated`

should be sufficient

Yeah I also noticed that ring_theory.int.basic works as well in your proof on cox, but I get the same results unfolding prime with the three imports. Is there a preference?

```
import algebra.associated
example {n : ℤ} (h : prime n) : ℤ :=
begin
unfold prime at h,
sorry
end
/-
n: ℤ
h: n ≠ 0 ∧ ¬is_unit n ∧ ∀ (a b : ℤ), n ∣ a * b → n ∣ a ∨ n ∣ b
⊢ ℤ
-/
```

```
import field_theory.finite.basic
example {n : ℤ} (h : prime n) : ℤ :=
begin
unfold prime at h,
sorry
end
/-
n: ℤ
h: n ≠ 0 ∧ ¬is_unit n ∧ ∀ (a b : ℤ), n ∣ a * b → n ∣ a ∨ n ∣ b
⊢ ℤ
-/
```

```
import ring_theory.int.basic
example {n : ℤ} (h : prime n) : ℤ :=
begin
unfold prime at h,
sorry
end
/-
n: ℤ
h: n ≠ 0 ∧ ¬is_unit n ∧ ∀ (a b : ℤ), n ∣ a * b → n ∣ a ∨ n ∣ b
⊢ ℤ
-/
```

#### Kevin Buzzard (Apr 12 2021 at 13:05):

It's the same function you're using every time.

Last updated: May 14 2021 at 21:11 UTC