Stupid question about gcd

Stream: new members

[Boldizsar Mann]

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]

Would you mind adding #backticks?

[Eric Wieser]

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

[Boldizsar Mann]

Any way of doing so without mathlib?

[Eric Wieser]

Yes, docs#classical.some

[Eric Wieser]

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

[Eric Wieser]

Perhaps we should find a way to highlight that better?

[Boldizsar Mann]

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

[Rémy Degenne]

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]

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]

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]

You're probably after docs#classical.some_spec

[Boldizsar Mann]

Okay, got it, nice, thanks!