lean_workbook_plus_38757
ProvedShow that divides where is a divisor of .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_38757 {y n : ℕ} (h : y ∣ n) : 2 ^ y - 1 ∣ 2 ^ n - 1 := by sorrySource
Show that divides where is a divisor of .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_38757 {y n : ℕ} (h : y ∣ n) : 2 ^ y - 1 ∣ 2 ^ n - 1 := by sorry