Coprime if product is squarefree

Stream: Is there code for X?

[Arend Mellendijk]

Am I right to say that we don't have the following lemma? It should hold more generally for PIDs or unique factorisation monoids depending on the definition of coprime you use.

import Mathlib.Data.Nat.Squarefree

theorem coprime_of_mul_squarefree (x y : ℕ) (h : Squarefree $ x * y) : x.coprime y := by
  by_contra h_ncop
  cases' Nat.Prime.not_coprime_iff_dvd.mp h_ncop with p hp
  exact (Nat.squarefree_iff_prime_squarefree.mp h) p hp.1 $ Nat.mul_dvd_mul hp.2.1 hp.2.2

[Yaël Dillies]

We seem to have exactly one lemma relating coprime and squarefree: nat.squarefree_mul

[Arend Mellendijk]

#5669

[Yury G. Kudryashov]

@Yaël Dillies Why do you keep posting links to mathlib3 docs even if the thread is about mathlib4?

[Kyle Miller]

Mathlib3: docs3#nat.squarefree_mul, Mathlib4: docs#Nat.squarefree_mul (Note these are both linkifiers Yaël. No need to make your own links)

[Yaël Dillies]

because that's the docs I have open and it's easy to figure out the mathlib4 declaration from there.

[Kevin Buzzard]

It's easier for everyone else if you post a less confusing message

[Junyan Xu]

Wow, a language model rewrote your proof: https://wolfia.com/query/01H4J8BPAGH5RQ0F2NEGZY1KSB (see here for context)
It seems to know Lean (3) pretty well and was able to informalize the proof (or maybe it already knew the proof); probably GPT(-4)?

[Scott Morrison]

That link doesn't seem germane to this thread?

[Junyan Xu]

Thanks, fixed

[Eric Rodriguez]

Can it generalise it?

[Junyan Xu]

I asked it to generalize (two of the attempts) but the results were disappointing. Anyway, here's a generalization by myself of the PR to arbitrary "decomposition monoids", which include all gcd monoids: https://gist.github.com/alreadydone/0ad7fb42db30711c4540ac92e37f6655 (probably golfable)

[Arend Mellendijk]

With that definition of RelPrime the original lemma actually holds for arbitrary commutative monoids!

import Mathlib.Algebra.Squarefree

theorem relPrime_of_squarefree_mul {M : Type _} [CommMonoid M]
  (x y : M) (h : Squarefree (x*y)) :
    ∀ (p : M), p ∣ x → p ∣ y → IsUnit p :=
  fun p hx hy => h p $ mul_dvd_mul hx hy

[Arend Mellendijk]

Ah sorry, I missed that you proved it too