lean_workbook_plus_15038
ProvedGiven , prove that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_15038 {a b c d : ℕ} (h : a^c ≡ b^c [ZMOD d]) : a^(2*c) ≡ b^(2*c) [ZMOD d] := by sorrySource
Given , prove that .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_15038 {a b c d : ℕ} (h : a^c ≡ b^c [ZMOD d]) : a^(2*c) ≡ b^(2*c) [ZMOD d] := by sorry