lean_workbook_plus_39529

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Let $p, q \in \mathbb{N}$ with $\gcd(p, q) = 1$ . Prove that for all $n \in \mathbb{N}$ , $\gcd(p^n, q^n) = 1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_39529 (p q : ℕ) (h : Nat.Coprime p q) (n : ℕ) : Nat.Coprime (p^n) (q^n)   :=  by sorry

Source