From 52564ecc0f6247fee8f9530162b2e8c36a2251b2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 27 Jun 2015 14:51:00 -0700
Subject: [PATCH] refactor(library/algebra/group_power): open namespaces in the
 "right" order

---
 library/algebra/group_power.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/algebra/group_power.lean b/library/algebra/group_power.lean
index 353f44add..d8bf80e28 100644
--- a/library/algebra/group_power.lean
+++ b/library/algebra/group_power.lean
@@ -92,7 +92,7 @@ theorem pow_inv_comm (a : A) : ∀m n, (a⁻¹)^m * a^n = a^n * (a⁻¹)^m
 
 end nat
 
-open int
+open nat int algebra
 
 definition ipow (a : A) : ℤ → A
 | (of_nat n) := a^n