lean_workbook_plus_42612

Proved

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

Case 1: $n=m$ \nOur expression equals $\frac{\gcd{(n,n)}}{n}\binom{n}{n}=1$ , which is an integer.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_42612  (n : ℕ)
  (h₀ : 0 < n) :
  ((Nat.gcd n n) / n * (n.choose n) : ℚ).den = 1   :=  by sorry

Source