chore(data/pprod): Add pprod.mk.eta (#5114)

This is exactly the same as prod.mk.eta
leanprover-community · Nov 27, 2020 · d3cc993 · d3cc993
1 parent 2c5d4a3
commit d3cc993
Showing 1 changed file with 14 additions and 0 deletions.
diff --git a/src/data/pprod.lean b/src/data/pprod.lean
@@ -0,0 +1,14 @@
+/-
+Copyright (c) 2020 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+
+/-!
+# Extra facts about `pprod`
+-/
+
+variables {α : Sort*} {β : Sort*}
+
+@[simp] lemma pprod.mk.eta {p : pprod α β} : pprod.mk p.1 p.2 = p :=
+pprod.cases_on p (λ a b, rfl)