Prove2Me

A factorial quotient for repeated letters

Proved
WorkbookSource.problem_28161

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

basically arranging DUUURRRD UUU RRR , which is 7!3!3!=140\frac{7!}{3! 3!} = \boxed{140}

Source: InternLM Lean-Workbook, record lean_workbook_28161 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.problem_28161 :
  7! / (3! * 3!) = 140  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_28161; Apache-2.0

View graph