lean_workbook_plus_30951
ProvedIf then prove that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_30951 (a b : ℕ) (hab : Nat.Coprime a b) : Nat.Coprime (a^2 + b^2) (a^2 * b^2) := by sorry
Source
If then prove that .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_30951 (a b : ℕ) (hab : Nat.Coprime a b) : Nat.Coprime (a^2 + b^2) (a^2 * b^2) := by sorry