## Stream: new members

### Topic: Stupid question about gcd

#### Boldizsar Mann (Apr 28 2021 at 17:32):

Hi, I have been trying to introduce a new natural number type called N and I was struggling with the definition of the gcd. i can prove lemma gcd_exists (a b : N) : (a ≠ 0 ∨ b ≠ 0) → ∃ d : N, (d ∣ a ∧ d ∣ b ∧ ¬ (∃ e : N, (e ∣ a ∧ e ∣ b ∧ d < e))), but how do I define the gcd then?

#### Eric Wieser (Apr 28 2021 at 17:35):

Would you mind adding #backticks?

#### Eric Wieser (Apr 28 2021 at 17:36):

docs#classical.some converts a proof of existence into a definition using the axiom of choice

#### Boldizsar Mann (Apr 28 2021 at 17:40):

Any way of doing so without mathlib?

#### Eric Wieser (Apr 28 2021 at 17:46):

(it's part of core lean, hence the "core/" at the top of the page)

#### Eric Wieser (Apr 28 2021 at 17:47):

Perhaps we should find a way to highlight that better?

#### Boldizsar Mann (Apr 28 2021 at 17:54):

Thank you! What can I do about it being noncomputable, because "it depends on 'classical.some' "?

#### Rémy Degenne (Apr 28 2021 at 17:58):

add noncomputable in front of the lemma, or add noncomputable theory at the top of the file, if you don't want to mark every lemma individually

#### Rémy Degenne (Apr 28 2021 at 18:01):

and if you want to read about the reason behind that noncomputable attribute: https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html

#### Boldizsar Mann (Apr 28 2021 at 18:08):

Okay, I will read it in detail. One more question: Can I have the "axioms" of the gcd as theorems I can refer to?

#### Eric Wieser (Apr 28 2021 at 18:19):

You're probably after docs#classical.some_spec

#### Boldizsar Mann (Apr 28 2021 at 18:29):

Okay, got it, nice, thanks!

Last updated: Dec 20 2023 at 11:08 UTC