From f4cbd98692ac71f521f5ca71a697f38f98ea5dbf Mon Sep 17 00:00:00 2001
From: Haitao Zhang <zhtprog@gmail.com>
Date: Wed, 15 Jul 2015 18:43:47 -0700
Subject: [PATCH] feat(library/algebra/group): add theorem eq_inv_of_mul_eq_one

---
 library/algebra/group.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/library/algebra/group.lean b/library/algebra/group.lean
index 24c402391..f5a8d180c 100644
--- a/library/algebra/group.lean
+++ b/library/algebra/group.lean
@@ -206,6 +206,9 @@ section group
   theorem eq_inv_iff_eq_inv (a b : A) : a = b⁻¹ ↔ b = a⁻¹ :=
   iff.intro !eq_inv_of_eq_inv !eq_inv_of_eq_inv
 
+  theorem eq_inv_of_mul_eq_one {a b : A} (H : a * b = 1) : a = b⁻¹ :=
+  begin rewrite [eq_inv_iff_eq_inv], apply eq.symm, exact inv_eq_of_mul_eq_one H end
+
   theorem mul.right_inv (a : A) : a * a⁻¹ = 1 :=
   calc
     a * a⁻¹ = (a⁻¹)⁻¹ * a⁻¹ : inv_inv