Commit 2026-04-28 10:12 1fd32e21

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