lean_workbook_plus_47996
ProvedProve that if .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_47996 : ∀ {a a' m : ℕ}, a ≡ a' [ZMOD m] → ∀ n : ℕ, a ^ n ≡ a' ^ n [ZMOD m] := by sorrySource
Prove that if .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_47996 : ∀ {a a' m : ℕ}, a ≡ a' [ZMOD m] → ∀ n : ℕ, a ^ n ≡ a' ^ n [ZMOD m] := by sorry