Generalize Odd.neg_zpow

Stream: mathlib4

[Alex Brodbelt]

I need this generalization for something I am working on. I believe this version is not in mathlib, if this is so I can open a PR.

import Mathlib

-- Does it really require a group or can we get away with DivisionMonoid like in Even.neg_zpow ?
-- Yes, cannot be DivisionMonoid as zpow_add requires inverses to be able to induct on integers.
variable variable {α : Type*} [Group α] [HasDistribNeg α] {a : α} {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 even_zero
  obtain ⟨k, rfl⟩ := h
  simp_rw [zpow_add, Even.neg_zpow (Even.mul_right even_two _), zpow_one, ← neg_mul_comm, ← neg_mul]

theorem Odd.neg_one_zpow' (h : Odd n) : (-1 : α) ^ n = -1 := by rw [h.neg_zpow', one_zpow]

-- Generalizes
#check Odd.neg_zpow

#check Odd.neg_one_zpow

-- (Sanity check from here on)
-- Because
variable (D : Type*) [DivisionRing D]

instance : Group Dˣ := by exact Units.instGroup

instance : HasDistribNeg Dˣ := by exact Units.instHasDistribNeg

-- Where any nonzero element is a unit
#check Ne.isUnit

[Artie Khovanov]

Can't find anything, I think this is new!
You should probably also prove the GroupWithZero version to make the specialisation back to rings easier.