feat(data/prod): add id_prod

leanprover-community · Sep 20, 2018 · d0f1b21 · d0f1b21
1 parent 318ec36
commit d0f1b21
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/data/prod.lean b/data/prod.lean
@@ -35,6 +35,9 @@ by rw [← @mk.eta _ _ p, ← @mk.eta _ _ q, mk.inj_iff]
 lemma ext {α β} {p q : α × β} : p.1 = q.1 → p.2 = q.2 → p = q :=
 by rw [ext_iff] ; intros ; split ; assumption
 
+lemma id_prod : (λ (p : α × α), (p.1, p.2)) = id :=
+by ext ; simp
+
 /-- Swap the factors of a product. `swap (a, b) = (b, a)` -/
 def swap : α × β → β × α := λp, (p.2, p.1)