brocard_4
Closed
Theorem & proof
·
brocard_4.lean
·
✓ verified
1
2
3
import Mathlib theorem brocard_4 : Nat.factorial 4 + 1 = 5 ^ 2 := by decide
Rewards pledged
No rewards pledged yet.