Skip to content

Commit

Permalink
fix: rename and.swap to And.swap (leanprover#389)
Browse files Browse the repository at this point in the history
  • Loading branch information
dwrensha committed Aug 26, 2022
1 parent e877b4d commit 362fc2d
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Init/Logic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,7 @@ variable {a b c d : Prop}

def And.elim (f : a → b → α) (h : a ∧ b) : α := f h.1 h.2

lemma and.swap : a ∧ b → b ∧ a :=
lemma And.swap : a ∧ b → b ∧ a :=
λ ⟨ha, hb⟩ => ⟨hb, ha⟩

lemma And.symm : a ∧ b → b ∧ a | ⟨ha, hb⟩ => ⟨hb, ha⟩
Expand Down

0 comments on commit 362fc2d

Please sign in to comment.