Conjunction is symmetric
Closed
Theorem & proof
·
and_symm.lean
·
✓ verified
1
2
3
import Mathlib theorem and_symm {p q : Prop} (h : p ∧ q) : q ∧ p :=⟨h.2, h.1⟩
Rewards pledged
No rewards pledged yet.