feat port: GroupTheory.GroupAction.Group (#1146)

leanprover-community · Dec 22, 2022 · e0d4c04 · e0d4c04
1 parent 0a5db45
commit e0d4c04
Show file tree

Hide file tree

Showing 3 changed files with 399 additions and 2 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -289,6 +289,7 @@ import Mathlib.Data.Vector
 import Mathlib.Dynamics.FixedPoints.Basic
 import Mathlib.GroupTheory.EckmannHilton
 import Mathlib.GroupTheory.GroupAction.Defs
+import Mathlib.GroupTheory.GroupAction.Group
 import Mathlib.GroupTheory.GroupAction.Opposite
 import Mathlib.GroupTheory.GroupAction.Option
 import Mathlib.GroupTheory.GroupAction.Pi

diff --git a/Mathlib/Data/Int/Basic.lean b/Mathlib/Data/Int/Basic.lean
@@ -77,11 +77,11 @@ lemma natAbs_cast (n : ℕ) : natAbs ↑n = n := rfl
 protected lemma coe_nat_sub {n m : ℕ} : n ≤ m → (↑(m - n) : ℤ) = ↑m - ↑n := ofNat_sub
 
 -- TODO restore @[to_additive coe_nat_zsmul]
-@[norm_cast]
+@[simp, norm_cast]
 theorem _root_.zpow_coe_nat [DivInvMonoid G] (a : G) (n : ℕ) : a ^ (Nat.cast n : ℤ) = a ^ n := zpow_ofNat ..
 @[simp]
 theorem _root_.coe_nat_zsmul [SubNegMonoid G] (a : G) (n : ℕ) : (n : ℤ) • a = n • a := ofNat_zsmul ..
-attribute [to_additive _root_.coe_nat_zsmul] _root_.zpow_coe_nat
+attribute [to_additive coe_nat_zsmul] zpow_coe_nat
 
 /-! ### Extra instances to short-circuit type class resolution