lean_workbook_plus_6471
ProvedProve that the if
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_6471 (a b x : ℕ) (hx: Nat.Coprime x b) : Nat.gcd a b = Nat.gcd (x * a) b := by sorry
Source
Prove that the if
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_6471 (a b x : ℕ) (hx: Nat.Coprime x b) : Nat.gcd a b = Nat.gcd (x * a) b := by sorry