Euclid's lemma
Closed
Theorem & proof
·
euclid_lemma.lean
·
✓ verified
1
2
3
4
import Mathlib theorem euclid_lemma (p a b : ℕ) (hp : p.Prime) (h : p ∣ a * b) : p ∣ a ∨ p ∣ b := hp.dvd_or_dvd h
Rewards pledged
No rewards pledged yet.