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

The lemmas `Even.neg_zpow` and `Even.neg_one_zpow` are stated assuming
  `[DivisionMonoid α] [HasDistribNeg α]`. However, `Odd.neg_zpow` and
  `Odd.neg_one_zpow` currently assume the stronger `[DivisionRing α]`.
  
  This PR weakens the assumption of the `Odd` lemmas to match their `Even`
  counterparts.
  
The lemmas are currently the only content of Mathlib.Algebra.Field.Power.
That files exists in order to "define Field with minimal imports". But after this PR, 
Power.lean does not rely on Mathlib.Algebra.Field.Defs any more. We hence deprecate 
"Field.Power" and move the two statements to Mathlib.Algebra.Ring.Int.Parity.

  ---
  
  
  Examples:
  ```
  -- these all work:
  example (z : ℤ) (h : Even z) : (-1 : ℂ)^z = 1 := Even.neg_one_zpow h
  example (z : ℤ) (h : Even z) : (-1 : unitary ℂ)^z = 1 := Even.neg_one_zpow h
  example (z : ℤ) (h : Odd z) : (-1 : ℂ)^z = -1 := Odd.neg_one_zpow h
  
  -- but this fails without the PR:
  example (z : ℤ) (h : Odd z) : (-1 : unitary ℂ)^z = -1 := Odd.neg_one_zpow h
  ```

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

Co-authored-by: DHTT <prparadoxes@gmail.com>
Co-authored-by: David Gross <david.gross@thp.uni-koeln.de>

Author: PrParadoxy

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

@@ -136,3 +136,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