lean_workbook_plus_58376

Proved

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

If gcd(a,b) is $1$ then $a$ and $b$ do not share ANY prime divisors. When squaring $a$ and $b$ , the exponents of each prime in the prime factorization are doubled. So, $a^2$ and $b^2$ will still not share any common divisors.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_58376  (a b : ℕ)
  (h₀ : Nat.gcd a b = 1) :
  Nat.gcd (a^2) (b^2) = 1   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph