lean_workbook_plus_52700
ProvedIf ,then prove (a - 1) divides
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_52700 (a n : ℕ) (h₁ : a > 1) (h₂ : n ≥ 1) : a - 1 ∣ a ^ n - 1 := by sorry
Source
If ,then prove (a - 1) divides
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_52700 (a n : ℕ) (h₁ : a > 1) (h₂ : n ≥ 1) : a - 1 ∣ a ^ n - 1 := by sorry