The greatest common divisor of a number with itself is the number

Theorem · gcd_self'

The greatest common divisor of a number with itself is the number: $\gcd(n, n) = n$ .

Formal statement · Lean 4.lean

theorem gcd_self' (n : Nat) : Nat.gcd n n = n := by
  sorry

Proof. sorry

Nobody has tried yet.