split(algebra/hom/ring): Split off algebra.ring.basic (#14144)

Move `non_unital_ring_hom` and `ring_hom` to a new file `algebra.hom.ring`. Crediting * Amelia for #1305 * Jireh for #13430
leanprover-community · May 17, 2022 · 65bf134 · 65bf134
1 parent 4ae5e7a
commit 65bf134
Show file tree

Hide file tree

Showing 8 changed files with 558 additions and 563 deletions.
diff --git a/src/algebra/field/basic.lean b/src/algebra/field/basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2014 Robert Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Lewis, Leonardo de Moura, Johannes Hölzl, Mario Carneiro
 -/
-import algebra.ring.basic
+import algebra.hom.ring
 
 /-!
 # Fields and division rings

diff --git a/src/algebra/group_power/basic.lean b/src/algebra/group_power/basic.lean
@@ -3,9 +3,8 @@ Copyright (c) 2015 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis
 -/
+import algebra.hom.ring
 import data.nat.basic
-import tactic.monotonicity.basic
-import group_theory.group_action.defs
 
 /-!
 # Power operations on monoids and groups