lean_workbook_plus_47673
ProvedProve that if , where is the greatest common divisor of and , then , for all .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_47673 (a b : ℕ) (hab : Nat.Coprime a b) (n : ℕ) : Nat.Coprime a (b^n) := by sorry
Source