Conjunction is idempotent
Closed
Theorem & proof
·
and_self_idem.lean
·
✓ verified
1
2
3
import Mathlib theorem and_self_idem (p : Prop) : (p ∧ p) ↔ p := by tauto
Rewards pledged
No rewards pledged yet.