Divisibility of by , , and
ProvedAlfutovaUstinov.problem_4_108This is Problem 4.108 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 an exponent such that is divisible by (a) , (b) , (c) , (d) ; the book's answer is .
The formal statement records the complete answer. For every natural number and for each modulus ,
In particular is the smallest positive exponent that works in all four cases (note and ).
The exercise concerns the multiplicative order of modulo small primes, which governs the period length of decimal fractions such as and .
Formalization Note The four parts are combined into one conjunction of equivalences, quantified over all (the case is harmless: is divisible by everything and ). The subtraction is natural-number subtraction, which is exact because .
import Mathlib
namespace AlfutovaUstinov
theorem problem_4_108 (n : ℕ) :
(7 ∣ 10 ^ n - 1 ↔ 6 ∣ n) ∧ (13 ∣ 10 ^ n - 1 ↔ 6 ∣ n) ∧
(91 ∣ 10 ^ n - 1 ↔ 6 ∣ n) ∧ (819 ∣ 10 ^ n - 1 ↔ 6 ∣ n) := by sorry
end AlfutovaUstinov