brocard_factor
Closed
Theorem & proof
·
brocard_factor.lean
·
✓ verified
1
2
3
4
5
import Mathlib theorem brocard_factor (n m : ℕ) (h : Nat.factorial n + 1 = (m + 1) ^ 2) : m * (m + 2) = Nat.factorial n := by have e : (m + 1) ^ 2 = m * (m + 2) + 1 := by ring omega
Rewards pledged
No rewards pledged yet.