lean_workbook_plus_49737
ProvedProve that if divides , then divides .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_49737 : ∀ {d n : ℕ}, d ∣ n → (2 ^ d - 1) ∣ (2 ^ n - 1) := by sorrySource
Prove that if divides , then divides .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_49737 : ∀ {d n : ℕ}, d ∣ n → (2 ^ d - 1) ∣ (2 ^ n - 1) := by sorry