prod version of nat.coprime.lcm_eq_mul

Stream: Is there code for X?

[Julian Külshammer]

The lemma nat.coprime.lcm_eq_mul states that if natural numbers a and b are coprime, then lcm a b = a * b. Does a version of this lemma for more than two elements exist, i.e. something like:

import data.list.range
import ring_theory.int.basic
import algebra.big_operators
import data.nat.log
import algebra.gcd_monoid.multiset
import algebra.gcd_monoid.finset

open_locale big_operators
open_locale classical

lemma finset.lcm_eq_prod_of_coprime {s : finset ℕ} (h : ∀ p q ∈ s, p ≠ q → nat.coprime p q) :
  ∏ p in s, p = s.lcm id :=
begin
  sorry
end

[Yury G. Kudryashov]

You should use docs#set.pairwise for h

[Yury G. Kudryashov]

Probably we don't have this lemma.

[Yury G. Kudryashov]

Note that the name should mention nat somewhere

[Julian Külshammer]

Thanks. I will try to understand how the pairwise comes in after having proved the lemma. The following is my current attempt. I feel like I am simply missing some generalizing trick.

import data.list.range
import ring_theory.int.basic
import algebra.big_operators
import data.nat.log
import algebra.gcd_monoid.multiset
import algebra.gcd_monoid.finset



open_locale big_operators
open_locale classical

lemma nat.coprime_prod_of_pairwise_coprime {s : finset ℕ} {x : ℕ} (h : ∀ p ∈ s, nat.coprime x p) :
  nat.coprime x (∏ (p : ℕ) in s, p) :=
begin
  apply finset.induction_on s,
  { simp only [nat.coprime_one_right_iff, finset.prod_empty], },
  { intros y t hynt ih,
    rw finset.prod_insert hynt,
    refine nat.coprime.mul_right _ ih,
     sorry },
end


lemma finset.nat.lcm_eq_prod_of_coprime {s : finset ℕ} (h : ∀ p q ∈ s, p ≠ q → nat.coprime p q) :
  ∏ p in s, p = s.lcm id :=
begin
  apply finset.induction_on s,
  { simp only [finset.prod_empty, finset.lcm_empty], },
  { intros x t hxnt ih,
    rw finset.prod_insert hxnt,
    rw finset.lcm_insert,
    rw ←ih,
    have hco : nat.coprime x (∏ (p : ℕ) in t, p),
      { apply nat.coprime_prod_of_pairwise_coprime,
        sorry },
    rw id.def,
    rw lcm_eq_nat_lcm,
    rw hco.lcm_eq_mul },
end

[Ruben Van de Velde]

Try starting your first proof with

  induction s using finset.induction_on with y t hynt ih,

That should make it pretty straightforward

[Julian Külshammer]

Thanks. I just looked again in the docs and found finset.induction_on' which works much better.

[Ruben Van de Velde]

Or revert h, before apply finset.induction_on s,, but I didn't try that

[Julian Külshammer]

@Yury G. Kudryashov How would I go about formulating h using pairwise?

[Julian Külshammer]

Ah, got it. You need coe_t to convert a finset to a set.

[Yury G. Kudryashov]

We should generalize set.pairwise to has_mem.

[Yaël Dillies]

Unfortunately, pairwise is already taken globally

[Yury G. Kudryashov]

pairwise_on?

[Yaël Dillies]

You won me!

[Yaël Dillies]

That's actually even better than the current state of things because open set often results in rapid death by ambiguity.