Coprime integers can't be both zero in a non-trivial ring

Stream: Is there code for X?

[Jz Pan]

Does mathlib have this little lemma?

-- ignore this import, I couldn't find a smaller one
import Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

universe u

lemma test (R : Type u) [CommRing R] [Nontrivial R] {a b : ℕ} (h : a.gcd b = 1) :
    (a : R) ≠ 0 ∨ (b : R) ≠ 0 := by
  apply not_or_of_imp
  intro ha hb
  exact one_ne_zero <| calc
    (1 : R) = (a : R) * Nat.gcdA a b + (b : R) * Nat.gcdB a b := by
      norm_cast
      simp only [← a.gcd_eq_gcd_ab b, h, Nat.cast_one, Int.cast_one]
    _ = (0 : R) := by rw [ha, hb, zero_mul, zero_mul, zero_add]

example (R : Type u) [CommRing R] [Nontrivial R] : (2 : R) ≠ 0 ∨ (3 : R) ≠ 0 :=
  test R (show (Nat.gcd 2 3) = 1 from by norm_num1)

This is useful, for example, to show at least one of 2 and 3 is invertible in a field.

[Anne Baanen]

We have docs#not_isCoprime_zero_zero, but I can't see yet how to easily connect Nat.gcd = 1 with isCoprime.

[Anne Baanen]

So I suppose the question is: is taking the contrapositive in this way enough to justify a new lemma? And since it's not just the contrapositive but also adding equality hypotheses and pushing the negation through an and, my answer would be yes.

[Kyle Miller]

@Anne Baanen There's docs#Int.isCoprime_iff_gcd_eq_one and docs#Int.coe_nat_gcd

[Anne Baanen]

Aren't those only for integers? The statement is about casting to any ring R.

[Kyle Miller]

I didn't mean to suggest these are everything, but it's the only real way to connect Nat.gcd = 1 to IsCoprime involving Nat. The definition of IsCoprime on Nat itself is not good. (This thread explores some of the issues.)

[Anne Baanen]

It's a good suggestion though. I suppose with docs#IsCoprime.map and some rewriting of coercions to algebra maps we'd be able to get there.

[Riccardo Brasca]

Oh gosh, IsCoprime (2 : ℕ) (3 : ℕ) is false!

[Jz Pan]

Maybe a.gcd b = 1 implies IsCoprime (a : Int) (b : Int) (in fact this is basically a.gcd_eq_gcd_ab b), and then by IsCoprime.map we obtain IsCoprime (a : R) (b : R).

[Riccardo Brasca]

Casting to a Ring seems OK, the point is that the definition is wrong for Semiring (in particular for ℕ...)

[Kevin Buzzard]

What do you propose for a definition for semirings then? We already had this discussion in the other thread and it's not so easy.

[Riccardo Brasca]

This is a good question :sweat_smile:

[Riccardo Brasca]

Maybe we should have IsCoprime only for Ring R, with a note suggesting to use Nat.gcd for Nat.

[Ruben Van de Velde]

Riccardo Brasca said:

Maybe we should have IsCoprime only for Ring R, with a note suggesting to use Nat.gcd for Nat.

And then maybe we can add an abbreviation for Nat.gcd a b = 1? :innocent:

[Eric Wieser]

That already exists, it's docs#Nat.coprime ?

[Matthew Ballard]

IsCoprime seems oddly named. I would expect the name to communicate something about spanning R.

[Kyle Miller]

@Matthew Ballard Isn't that what IsCoprime is about? Spanning R and being able to get 1 are the same thing, right?

[Matthew Ballard]

Right, I would expect it not to be called IsCoprime and to be called e.g. MemSpanOne

[Jz Pan]

Kevin Buzzard said:

What do you propose for a definition for semirings then? We already had this discussion in the other thread and it's not so easy.

Is this a good definition? ∃ a b c d, a * x + b * y = 1 + c * x + d * y:see_no_evil:

[Jz Pan]

Then for Nat, a.gcd b = 1 indeed implies IsCoprime a b

[Matthew Ballard]

That certainly seems better but I don't know how easy it is to work with. Is there any API for talking about formal differences in R?

[Kyle Miller]

@Jz Pan See around here; that idea came up in the thread. Michael Stoll strongly suggested not pursuing it as a definition for IsCoprime, but suggested perhaps having Semiring.IsCoprime with that definition.

[Riccardo Brasca]

Riccardo Brasca said:

Maybe we should have IsCoprime only for Ring R, with a note suggesting to use Nat.gcd for Nat.

I just realized that this is a bad idea. IsCoprime is a useful notion for Ideal R, that is only a Semiring.

[Riccardo Brasca]

We want this to stay true (it's in flt-regular, I don't know why we stated it using negation on both sides...).

theorem not_coprime_not_top {S : Type _} [CommRing S] (a b : Ideal S) :
    ¬IsCoprime a b ↔ a + b ≠ ⊤ :=

[Eric Wieser]

Eric Wieser said:

That already exists, it's docs#Nat.coprime ?

... which doesn't match the naming convention: https://github.com/leanprover/std4/pull/187