X^d - 1 | X^(nd) - 1

Stream: Is there code for X?

[Gareth Ma]

Hi, is there any existing code on the formula a^d - 1 | a^(nd) - 1 over the integers? Or if it is somehow easier, the formula X^d - 1 | X^(nd) - 1, where d and n are integers?
If not, can someone point me to how I should express the polynomial P = sum(X^(id), 0 <= i < n), as well as how I will expand P * (X^d - 1)? All the work seems quite trivial on paper, but I have not dealt with variable-number sums in Lean before, and shifting indices / cancellations sounds quite annoying.

[Gareth Ma]

I think another easier way is to prove X - 1 | X^n - 1, then substitute X <- X^d? But if someone can guide me on that it will be great :pleading_face:

[Gareth Ma]

Nevermind, I found https://leanprover-community.github.io/mathlib_docs/algebra/geom_sum.html#geom%E2%82%82_sum

[Kevin Buzzard]

import tactic
import algebra.geom_sum

open_locale big_operators -- so I can use ∑

open finset -- so I don't have to write `finset.range`

example (a b : ℤ) (n d : ℕ) : a ^ d - 1 ∣  a ^ (n * d) - 1 :=
begin
  use ∑ i in range n, (a ^ d) ^ i,
  rw [mul_comm (a ^ d - 1), geom_sum_mul],
  ring_exp,
end

[Junyan Xu]

I think another easier way is to prove X - 1 | X^n - 1, then substitute X <- X^d? But if someone can guide me on that it will be great :plea

It seems we don't have polynomial.comp_dvd_comp but we do have docs#polynomial.mul_comp

[Gareth Ma]

That path seems quite complicated, and the geom_sum is working fine

[Gareth Ma]

However, I am struggling with some issue. Essentially I am trying to prove the a ^ d - 1 | a ^ (n * d) - 1 for mersenne numbers, i.e. mersenne d | mersenne (n * d). However, mersenne returns a ℕ, while the geom_sum returns a ℤ. Is there any way to convert them easily?
Here is my extremely messy code, I can prove that the divisibility holds over the integers, but the natural numbers are not a ring and so subtraction causes many problems as always.

-- I forgot how to name this
theorem int_dvd_imp_nat_dvd {m n : ℕ} :
int.of_nat m ∣ int.of_nat n → m ∣ n :=
begin
  rintros ⟨d, hd⟩,
  use int.to_nat d,
  sorry -- given n ≥ 0, m ≥ 0, n = d * m over ℤ, prove n = d * m over ℕ
end

theorem pow_div {m n : ℕ} (a : ℤ) (h : m ∣ n) : (a ^ m - 1) ∣ (a ^ n - 1) :=
begin
  let d : ℕ := n / m,
  use ∑ i in range d, (a ^ m) ^ i,
  rw [mul_comm (a ^ m - 1), geom_sum_mul],
  rw [← pow_mul', (nat.dvd_iff_div_mul_eq n m).1 h],
end

-- Type coercion hell
theorem mersenne_div {m n : ℕ} (h : m ∣ n) : mersenne m ∣ mersenne n :=
begin
  cases pow_div 2 h with d hd,
  unfold mersenne,
  apply int_dvd_imp_nat_dvd,
  use d,
  -- ?????
end

Do you mind helping as well

[Kevin Buzzard]

theorem int_dvd_imp_nat_dvd {m n : ℕ} : (m : ℤ) ∣ (n : ℤ) → m ∣ n :=
begin
  intro h,
  exact_mod_cast h,
end

It used to be a total pain moving between nat and int and rat, but the cast tactics (norm_cast, push_cast, exact_mod_cast) etc can do it as long as you use the so-called "simp normal form" for casts, which is to use coercions (the little up-arrow) rather than the names of the functions they represent (for example int.of_nat).

[Kevin Buzzard]

example (n : ℕ) : int.of_nat n = (n : ℤ) := rfl

They're equal by definition, but many tactics (like simp, rw and the cast tactics) work up to syntactic equality, not just definitional equality. If we had X lemmas about ↑n and we wanted them to also apply to int.of_nat n then because these tactics work up to syntactic equality we'd have to have X more lemmas about int.of_nat n. The trick is to try and keep your code always in the "canonical" form which the library designers have chosen for each mathematical idea, and the canonical map from nat to int is ↑n, sometimes expressed (n : ℤ), rather than int.of_nat.

[Kevin Buzzard]

-- I forgot how to name this, so let's see what Lean calls it
theorem int_dvd_imp_nat_dvd {m n : ℕ} : (m : ℤ) ∣ n → m ∣ n :=
begin
  library_search, -- exact int.coe_nat_dvd.mp
end

The bi-implication is called int.coe_nat_dvd and probably we don't have a name for the one-sided implication (we just rewrite with the bi-implication).

Alternatively

-- I forgot how to name this, so let's see what Lean calls it
theorem int_dvd_imp_nat_dvd {m n : ℕ} : (m : ℤ) ∣ n → m ∣ n :=
begin
  intro h,
  show_term {exact_mod_cast h}, -- see the proof that the tactic generated
end

you can see how the cast tactic proves it and learn the name from that.

[Kevin Buzzard]

I can't answer your last question because your code isn't a #mwe so I can't see the exact definition of mersenne. Click on the #mwe link to learn about how to write a good question.

[Gareth Ma]

Thank you so much! Somehow my library_search couldn't find that case, maybe my original formulation was too weird/messy for it to find the correct clause - show_term will help me a lot too haha. Also, mersenne is from number_theory.lucas_lehmer, which is just 2^n - 1 over ℕ

def mersenne (p : ℕ) : ℕ := 2^p - 1

[Kevin Buzzard]

theorem mersenne_div {m n : ℕ} (h : m ∣ n) : 2 ^ m - 1 ∣ 2 ^ n - 1 :=
begin
  rw ← int.coe_nat_dvd, -- annoying because you're not really supposed to need to know the names of these lemmas
  convert pow_div 2 h;
  { rw nat.cast_sub,
    { norm_cast, },
    exact nat.one_le_pow' _ 1, }, -- thanks `library_search`
end

[Kevin Buzzard]

After convert there are two very similar goals. The semicolon means "apply the following tactic to both of them", and the { } means "treat all these tactics as one tactic".

[Yaël Dillies]

Kevin Buzzard said:

The bi-implication is called int.coe_nat_dvd and probably we don't have a name for the one-sided implication (we just rewrite with the bi-implication).

In fact, we do: docs#has_dvd.dvd.nat_cast

[Niels Voss]

I got the proof down to two lines

import tactic
import algebra.geom_sum

theorem mersenne_div {m n : ℕ} (h : m ∣ n) : 2 ^ m - 1 ∣ 2 ^ n - 1 :=
begin
  rcases h with ⟨k, rfl⟩,
  simpa only [pow_mul, one_pow] using nat_sub_dvd_pow_sub_pow _ 1 _,
end

I actually had the exact same problem when writing my pseudoprimes PR so I actually wrote nat_sub_dvd_pow_sub_pow a month or so ago for this specific purpose.

[Niels Voss]

Here is the link to the thread where I originally discussed this: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/divisibilty.20of.20powers