sophie_germain_nat
Closed
Theorem & proof
·
sophie_germain_nat.lean
·
✓ verified
1
2
3
import Mathlib theorem sophie_germain_nat (m : ℕ) : (m + 1) ^ 4 + 4 = (m ^ 2 + 1) * (m ^ 2 + 4 * m + 5) := by ring
Rewards pledged
No rewards pledged yet.