number theory

Stream: mathlib4

[BANGJI HU]

import Mathlib.NumberTheory.ArithmeticFunction
import Mathlib.Tactic

open Nat
def euler_phi (n : ℕ) : ℕ := (Nat.totient n)


theorem problem_statement (n : ℕ) (hn : 0 < n) :
  2^(n * (n + 1)) ∣ 32 * euler_phi (2^(2^n) - 1) :=by
rw [euler_phi]

[BANGJI HU]

is it proof in mathlib?

[Damiano Testa]

Is hn needed?

[BANGJI HU]

This problem is summarized (the right can be decomposed by the square difference formula) and then analyzes the content of 2^(2^(n-1))+1 prime factor 2 (the highest power divisible by 2) to prove that the order of 2 modulo p is 2^n, and introduces 2^n divisible p-1 If there are two prime factors, it is done, if it is a prime number, then the Euler function is 2^(2^(n-1)), and the remaining case ≥ 2n is only ≥ 2nd power of the prime number

[BANGJI HU]

import Mathlib.NumberTheory.ArithmeticFunction
import Mathlib.Tactic

open Nat
def euler_phi (n : ℕ) : ℕ := Nat.totient n


lemma diff_of_squares (a b : ℕ) : (a ^ 2 - b ^ 2) = (a - b) * (a + b) := by
  ring_nf
  rw [Nat.pow_two_sub_pow_two]
  ring
theorem problem_statement (n : ℕ) (hn : 0 < n) :
  2^(n * (n + 1)) ∣ 32 * euler_phi (2^(2^n) - 1) := by
  rw [euler_phi]
  induction n with k hk generalizing n
  case one =>

[BANGJI HU]

seem to be have trouble at induction n with k hk generalizing n

[Thobias Rex Smite]

Did you solve this? What do you expect to get from generalizing? @hand bob