PR summary 6f097b9016

Import changes

No significant changes to the import graph

Declarations diff

+ pow_of_pow_add_prime

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

Unclear what and why is failing...

Run lake exe mk_all in terminal then push again. This is required when you create a new file.

Thanks. Discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/PR.20fail.3A.20Error.3A.20Process.20completed.20with.20exit.20code.201.2E

Should this go into archive or mathlib proper?

Thank for the review. I think some proof of this should go in Mathlib, but not sure about this one. Other proofs can be found or are linked in https://math.stackexchange.com/questions/140804/if-2n1-is-prime-why-must-n-be-a-power-of-2, and there is the one in Harvey & Wright mentioned in this PR. I do not know if these are shorter / more elegant.

I would be in favor of this result going into mathlib with a more streamlined proof.

I would be in favor of this result going into mathlib with a more streamlined proof.

Do you think this specific approach can be substantially streamlined? Or do you think another approach would result in what could go in Mathlib? I might take this up then, but it wouldn't affect this PR, I guess.

I would be in favor of this result going into mathlib with a more streamlined proof.

Maybe I misunderstood. Did you mean mathlib or mathlib/Mathlib?

I meant mathlib/Mathlib. I think a more direct approach would probably be better. Perhaps something along the lines of this:

theorem Nat.exists_eq_two_pow_mul_odd {n : ℕ} (hn : n ≠ 0) : ∃ k m : ℕ, Odd m ∧ n = 2 ^ k * m :=
  let ⟨k, m, hm, hn⟩ := Nat.exists_eq_pow_mul_and_not_dvd hn 2 (Nat.succ_ne_self 1)
  ⟨k, m, Nat.odd_iff_not_even.mpr (mt Even.two_dvd hm), hn⟩

theorem Odd.nat_add_one_dvd_pow_add_one (x : ℕ) {n : ℕ} (hn : Odd n) : x + 1 ∣ x ^ n + 1 := by
  simpa only [one_pow] using hn.nat_add_dvd_pow_add_pow x 1

theorem H3 (a n : ℕ) (ha : 1 < a) (hn : 1 < n) (hP : Nat.Prime (a ^ n + 1)) :
    ∃ m : ℕ, n = 2 ^ m := by
  obtain ⟨k, m, hm, rfl⟩ := Nat.exists_eq_two_pow_mul_odd (one_pos.trans hn).ne'
  have key := hm.nat_add_one_dvd_pow_add_one (a ^ 2 ^ k)
  rw [pow_mul] at hP
  sorry

Remarkable reduction, many thanks. I used this, and you can see the result in the last commit, which I hope is not too bad. I think this commit (after I have reduced it further) will then be split into several PRs because the lemmas belong to different parts of Mathlib. This PR will depend on them and the code will move to Nat.Prime. All with attribution. That's my idea. What do you think?

@tb65536 where to put the final theorem? I looked at Data.Nat.Prime but adding the import of Data.Nat.Factorization.Basic (because of #14166) creates a circular dependency. We also need to import Algebra.GeomSum (#14180) and Data.Nat.Defs (#14183). These are all short so their body could just be copied without importing them. I might just do that.

No, copying won't work because of Nat.exists_eq_pow_mul_and_not_dvd which would also be needed from Factorization.Basic. So, Data.Nat.Prime is not the right place. I also think Data.Nat.Prime is too fat and should be split.

This PR/issue depends on:

• [Merged by Bors] - chore(Data/Nat): refactor import of Nat/Prime by Nat/Factors #14357
  By Dependent Issues (🤖). Happy coding!