lean_workbook_plus_22832
ProvedProve that if , then . (What about the converse?)
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_22832 {a b : ℕ} (h : a ∣ b) : 2 ^ a - 1 ∣ 2 ^ b - 1 := by sorrySource
Prove that if , then . (What about the converse?)
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_22832 {a b : ℕ} (h : a ∣ b) : 2 ^ a - 1 ∣ 2 ^ b - 1 := by sorry