lean_workbook_plus_25000
ProvedProve that if , then .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_25000 (p k : ℕ) (x : Units (ZMod (p^k))) (hx : x^6 = 1) :
orderOf x ∣ 6 := by sorrySource
Prove that if , then .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_25000 (p k : ℕ) (x : Units (ZMod (p^k))) (hx : x^6 = 1) :
orderOf x ∣ 6 := by sorry