lean_workbook_plus_67066
ProvedIf , we have ,
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_67066 {m n : ℕ} (hmn: m ∣ n) : 2^m - 1 ∣ 2^n - 1 := by sorrySource
If , we have ,
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_67066 {m n : ℕ} (hmn: m ∣ n) : 2^m - 1 ∣ 2^n - 1 := by sorry