False implies anything
Closed
Theorem & proof
·
false_elim.lean
·
✓ verified
1
2
3
import Mathlib theorem false_elim {p : Prop} (h : False) : p := h.elim
Rewards pledged
No rewards pledged yet.