feat(Algebra/Field/Power): weaken assumptions of Odd.neg_zpow

Mathlib/Algebra/Field/Power.lean

@@ -3,34 +3,8 @@ Copyright (c) 2014 Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis, Leonardo de Moura, Johannes Hölzl, Mario Carneiro
 -/
-module
+module -- shake: keep-all
 
-public import Mathlib.Algebra.Field.Defs
 public import Mathlib.Algebra.Ring.Int.Parity
 
-/-!
-# Results about powers in fields or division rings.
-
-This file exists to ensure we can define `Field` with minimal imports,
-so it contains some lemmas about powers of elements which need imports
-beyond those needed for the basic definition.
--/
-
-public section
-
-
-variable {α : Type*}
-
-section DivisionRing
-
-variable [DivisionRing α] {n : ℤ}
-
-theorem Odd.neg_zpow (h : Odd n) (a : α) : (-a) ^ n = -a ^ n := by
-  have hn : n ≠ 0 := by rintro rfl; exact Int.not_even_iff_odd.2 h .zero
-  obtain ⟨k, rfl⟩ := h
-  simp_rw [zpow_add' (.inr (.inl hn)), zpow_one, zpow_mul, zpow_two, neg_mul_neg,
-    neg_mul_eq_mul_neg]
-
-theorem Odd.neg_one_zpow (h : Odd n) : (-1 : α) ^ n = -1 := by rw [h.neg_zpow, one_zpow]
-
-end DivisionRing
+deprecated_module (since := "2026-04-17")

Mathlib/Algebra/Ring/Int/Parity.lean

@@ -132,3 +132,23 @@ theorem coe_nat_two_pow_pred (p : ℕ) : ((2 ^ p - 1 : ℕ) : ℤ) = (2 ^ p - 1
   natCast_pow_pred 2 p (by decide)
 
 end Int
+
+section DivisionMonoid
+
+variable {α : Type*} [DivisionMonoid α] [HasDistribNeg α] {n : ℤ}
+
+theorem Odd.neg_zpow (h : Odd n) (a : α) : (-a) ^ n = -a ^ n := by
+  obtain ⟨k, rfl⟩ := h
+  cases k with
+  | ofNat k =>
+    rw [Int.ofNat_eq_natCast]
+    norm_cast
+    simp [pow_add]
+  | negSucc k =>
+    simp_rw [Int.negSucc_eq, show 2 * -(↑k + 1) + (1 : ℤ) = - (1 + k*2) by grind, _root_.zpow_neg]
+    norm_cast
+    simp [pow_add]
+
+theorem Odd.neg_one_zpow (h : Odd n) : (-1 : α) ^ n = -1 := by rw [h.neg_zpow, one_zpow]
+
+end DivisionMonoid

Mathlib/Tactic/FieldSimp/Lemmas.lean

@@ -6,7 +6,8 @@ Authors: Heather Macbeth, Arend Mellendijk, Michael Rothgang
 module
 
 public import Mathlib.Algebra.BigOperators.Group.List.Basic
-public import Mathlib.Algebra.Field.Power  -- shake: keep (Qq dependency)
+public import Mathlib.Algebra.Field.Defs  -- shake: keep (Qq dependency)
+public import Mathlib.Algebra.Ring.Int.Parity -- shake: keep (Qq dependency)
 public import Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
 public import Mathlib.Util.Qq