two_dvd_of_dvd_sq
Closed
Theorem & proof
·
two_dvd_of_dvd_sq.lean
·
✓ verified
1
2
3
import Mathlib theorem two_dvd_of_dvd_sq (n : ℕ) (h : 2 ∣ n ^ 2) : 2 ∣ n := Nat.Prime.dvd_of_dvd_pow Nat.prime_two h
Rewards pledged
No rewards pledged yet.