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