For which $n$ is $n^{2001}-n^{4}$ divisible by $11$ ?

Proved

AlfutovaUstinov.problem_4_112

by evgeth · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

congruenceselementary-number-theoryfermat-little-theoremnumber-theory

This is Problem 4.112 of N. B. Alfutova and A. V. Ustinov, Algebra and Number Theory (MCCME, 2002), Chapter 4, §4 “Theorems of Fermat and Euler”. The problem asks: for which $n$ is the number $n^{2001}-n^{4}$ divisible by $11$ ? The book's answer is: exactly for $n\equiv 0$ and $n\equiv 1 \pmod{11}$ .

Theorem. For every integer $n$ ,

11 \mid n^{2001}-n^{4} \iff n\equiv 0 \pmod{11}\ \text{ or }\ n\equiv 1 \pmod{11}.

This is a typical exercise on reducing a large exponent modulo a prime by means of Fermat's little theorem.

Formalization Note The variable $n$ ranges over all integers $\mathbb Z$ , and the congruences are expressed with Int.ModEq (notation n ≡ a [ZMOD 11]).

Preamble

import Mathlib

Formal statement

namespace AlfutovaUstinov

theorem problem_4_112 (n : ℤ) : 11 ∣ n ^ 2001 - n ^ 4 ↔ n ≡ 0 [ZMOD 11] ∨ n ≡ 1 [ZMOD 11] := by sorry

end AlfutovaUstinov

Source

N. B. Alfutova, A. V. Ustinov, «Алгебра и теория чисел. Сборник задач для математических школ» (Algebra and Number Theory: a problem book for mathematical schools), Moscow: MCCME, 2002, Chapter 4 «Арифметика остатков» (Arithmetic of residues), §4 «Теоремы Ферма и Эйлера» (Theorems of Fermat and Euler), Problem 4.112. Problem text and answer as catalogued on problems.ru, problem 60738: https://problems.ru/view_problem_details_new.php?id=60738

View graph

For which nnn is n2001−n4n^{2001}-n^{4}n2001−n4 divisible by 111111?

For which $n$ is $n^{2001}-n^{4}$ divisible by $11$ ?