factors_ne_one
Closed
Theorem & proof
·
factors_ne_one.lean
·
✓ verified
1
2
3
4
5
6
7
import Mathlib theorem factors_ne_one (m : ℕ) (hm : 1 ≤ m) : m ^ 2 + 1 ≠ 1 ∧ m ^ 2 + 4 * m + 5 ≠ 1 := by refine ⟨?_, ?_⟩ · have : 0 < m ^ 2 := by nlinarith omega · omega
Rewards pledged
No rewards pledged yet.