nat.coprime vs is_coprime

Stream: maths

[Yury G. Kudryashov]

Is there any reason to have both?

[Yury G. Kudryashov]

I mean, should we use is_coprime for natural numbers as well (and prove is_coprime m n ↔ gcd m n = 1 if this was not done yet)?

[Mario Carneiro]

This causes a pretty big dependency bump of some early files IIRC

[Yury G. Kudryashov]

Does it? data.nat.basic already depends on algebra.order.ring. ring_theory.coprime.basic also imports tactic.ring but it uses this tactic only once.

[Mario Carneiro]

Moving the definition of is_coprime to algebra.ring.basic (and any other lemmas that don't need any more dependencies than that) would probably be enough to resolve the issue

[Yury G. Kudryashov]

I remember that we had ∃ m n, m * a + n * b = gcd a b somewhere. Do you remember the name of the lemma?

[Mario Carneiro]

something about bezout or gcd_ab

[Mario Carneiro]

docs#nat.gcd_eq_gcd_ab

[Mario Carneiro]

oh right, I can never grep for this one because all the docs insist on putting the accent in

[Kevin Buzzard]

Guess you'll just have to Google for it in the docs

[Mario Carneiro]

I move to rename this lemma to nat.bezout

[Kevin Buzzard]

But that's explicitly anti mathlib naming conventions! We don't have binomial_theorem, we have add_pow etc

[Johan Commelin]

What's hard about grepping for gcd_ab?

[Mario Carneiro]

because we don't normally use variable names in the definition, so unless you remember that gcd_a or gcd_b are a thing you won't think to search for that

[Mario Carneiro]

I only remember this because I have to relearn how to search for bezout every 3 months

[Mario Carneiro]

Kevin Buzzard said:

But that's explicitly anti mathlib naming conventions! We don't have binomial_theorem, we have add_pow etc

Not entirely, there are certain combinations of symbols that have their own name like trans. Plus, I do think that we should not be using the symbol reading convention when there is another name that is more strongly associated to the lemma (e.g. a "named" theorem in maths)

[Mario Carneiro]

most named theorems have incredibly awkward symbol reading names

[Mario Carneiro]

Plus, we can always use aliases, which are an under-utilized tool

[Yury G. Kudryashov]

I see a reason to still have nat.coprime: it's about nat

[Yury G. Kudryashov]

is_coprime needs cast to int.

[Mario Carneiro]

oh, we can't have coprimality on semirings?

[Yury G. Kudryashov]

docs#is_coprime is defined in terms of Bezout

[Mario Carneiro]

oh I see, yeah that definition doesn't work for nat

[Yury G. Kudryashov]

Probably we can have a * x + b * y = a' * x + b' * y + 1 but this will make all proofs longer.

[Mario Carneiro]

It does apply to nat though, it might be fun to have a theorem characterizing what it means for nat

[Mario Carneiro]

I think is_coprime (x : nat) (y : nat) <-> x = 1 \/ y = 1

[Alex J. Best]

Did the chicken mcnugget theorem pr land yet (on mobile so no link sorry)? That's quite relevant to this sort of thing, generalizing bezout type theorems to semigroups