/-
Copyright (c) 2014 Robert Lewis. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Robert Lewis, Leonardo de Moura, Johannes Hölzl, Mario Carneiro

! This file was ported from Lean 3 source module algebra.field.power
! leanprover-community/mathlib commit 1e05171a5e8cf18d98d9cf7b207540acb044acae
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Field.Defs
import Mathlib.Algebra.GroupWithZero.Power
import Mathlib.Algebra.Parity

/-!
# Results about powers in fields or division rings.

This file exists to ensure we can define `Field` with minimal imports,
so contains some lemmas about powers of elements which need imports
beyond those needed for the basic definition.
-/


variable {
α: Type ?u.1342
α : 
Type _: Type (?u.2+1)
Type _}

section DivisionRing

variable [
DivisionRing: Type ?u.8 → Type ?u.8
DivisionRing 
α: Type ?u.5
α] {
n: ℤ
n : 
ℤ: Type
ℤ}

set_option linter.deprecated false in
@[simp]
theorem 
zpow_bit1_neg: ∀ {α : Type u_1} [inst : DivisionRing α] (a : α) (n : ℤ), (-a) ^ bit1 n = -a ^ bit1 n
zpow_bit1_neg (
a: α
a : 
α: Type ?u.13
α) (
n: ℤ
n : 
ℤ: Type
ℤ) : (-
a: α
a) ^ 
bit1: {α : Type ?u.30} → [inst : One α] → [inst : Add α] → α → α
bit1 
n: ℤ
n = -
a: α
a ^ 
bit1: {α : Type ?u.70} → [inst : One α] → [inst : Add α] → α → α
bit1 
n: ℤ
n := by
Goals accomplished! 🐙
  
α: Type u_1

inst✝: DivisionRing α

n✝: ℤ

a: α

n: ℤ

(-a) ^ bit1 n = -a ^ bit1 nrw [
α: Type u_1

inst✝: DivisionRing α

n✝: ℤ

a: α

n: ℤ

(-a) ^ bit1 n = -a ^ bit1 n
zpow_bit1': ∀ {G₀ : Type ?u.365} [inst : GroupWithZero G₀] (a : G₀) (n : ℤ), a ^ bit1 n = (a * a) ^ n * a
zpow_bit1',
α: Type u_1

inst✝: DivisionRing α

n✝: ℤ

a: α

n: ℤ

(-a * -a) ^ n * -a = -a ^ bit1 n 
α: Type u_1

inst✝: DivisionRing α

n✝: ℤ

a: α

n: ℤ

(-a) ^ bit1 n = -a ^ bit1 n
zpow_bit1': ∀ {G₀ : Type ?u.486} [inst : GroupWithZero G₀] (a : G₀) (n : ℤ), a ^ bit1 n = (a * a) ^ n * a
zpow_bit1',
α: Type u_1

inst✝: DivisionRing α

n✝: ℤ

a: α

n: ℤ

(-a * -a) ^ n * -a = -((a * a) ^ n * a) 
α: Type u_1

inst✝: DivisionRing α

n✝: ℤ

a: α

n: ℤ

(-a) ^ bit1 n = -a ^ bit1 n
neg_mul_neg: ∀ {α : Type ?u.519} [inst : Mul α] [inst_1 : HasDistribNeg α] (a b : α), -a * -b = a * b
neg_mul_neg,
α: Type u_1

inst✝: DivisionRing α

n✝: ℤ

a: α

n: ℤ

(a * a) ^ n * -a = -((a * a) ^ n * a) 
α: Type u_1

inst✝: DivisionRing α

n✝: ℤ

a: α

n: ℤ

(-a) ^ bit1 n = -a ^ bit1 n
neg_mul_eq_mul_neg: ∀ {α : Type ?u.761} [inst : Mul α] [inst_1 : HasDistribNeg α] (a b : α), -(a * b) = a * -b
neg_mul_eq_mul_neg
α: Type u_1

inst✝: DivisionRing α

n✝: ℤ

a: α

n: ℤ

(a * a) ^ n * -a = (a * a) ^ n * -a]
Goals accomplished! 🐙
#align zpow_bit1_neg 
zpow_bit1_neg: ∀ {α : Type u_1} [inst : DivisionRing α] (a : α) (n : ℤ), (-a) ^ bit1 n = -a ^ bit1 n
zpow_bit1_neg

theorem 
Odd.neg_zpow: ∀ {α : Type u_1} [inst : DivisionRing α] {n : ℤ}, Odd n → ∀ (a : α), (-a) ^ n = -a ^ n
Odd.neg_zpow (
h: Odd n
h : 
Odd: {α : Type ?u.903} → [inst : Semiring α] → α → Prop
Odd 
n: ℤ
n) (
a: α
a : 
α: Type ?u.895
α) : (-
a: α
a) ^ 
n: ℤ
n = -
a: α
a ^ 
n: ℤ
n := by
Goals accomplished! 🐙
  
α: Type u_1

inst✝: DivisionRing α

n: ℤ

h: Odd n

a: α

(-a) ^ n = -a ^ nobtain 
⟨k, rfl⟩: ∃ b, n = bit1 b
⟨
k: ℤ
k
⟨k, rfl⟩: ∃ b, n = bit1 b
, 
rfl: n = bit1 k
rfl
⟨k, rfl⟩: ∃ b, n = bit1 b
⟩ := 
h: Odd n
h.
exists_bit1: ∀ {α : Type ?u.1227} [inst : Semiring α] {a : α}, Odd a → ∃ b, a = bit1 b
exists_bit1
α: Type u_1

inst✝: DivisionRing α

a: α

k: ℤ

h: Odd (bit1 k)

intro
(-a) ^ bit1 k = -a ^ bit1 k
  
α: Type u_1

inst✝: DivisionRing α

n: ℤ

h: Odd n

a: α

(-a) ^ n = -a ^ nexact 
zpow_bit1_neg: ∀ {α : Type ?u.1297} [inst : DivisionRing α] (a : α) (n : ℤ), (-a) ^ bit1 n = -a ^ bit1 n
zpow_bit1_neg 
_: ?m.1298
_ 
_: ℤ
_
Goals accomplished! 🐙
#align odd.neg_zpow 
Odd.neg_zpow: ∀ {α : Type u_1} [inst : DivisionRing α] {n : ℤ}, Odd n → ∀ (a : α), (-a) ^ n = -a ^ n
Odd.neg_zpow

theorem 
Odd.neg_one_zpow: Odd n → (-1) ^ n = -1
Odd.neg_one_zpow (
h: Odd n
h : 
Odd: {α : Type ?u.1350} → [inst : Semiring α] → α → Prop
Odd 
n: ℤ
n) : (-
1: ?m.1379
1 : 
α: Type ?u.1342
α) ^ 
n: ℤ
n = -
1: ?m.1588
1 := by
Goals accomplished! 🐙 
α: Type u_1

inst✝: DivisionRing α

n: ℤ

h: Odd n

(-1) ^ n = -1rw [
α: Type u_1

inst✝: DivisionRing α

n: ℤ

h: Odd n

(-1) ^ n = -1
h: Odd n
h.
neg_zpow: ∀ {α : Type ?u.1736} [inst : DivisionRing α] {n : ℤ}, Odd n → ∀ (a : α), (-a) ^ n = -a ^ n
neg_zpow,
α: Type u_1

inst✝: DivisionRing α

n: ℤ

h: Odd n

-1 ^ n = -1 
α: Type u_1

inst✝: DivisionRing α

n: ℤ

h: Odd n

(-1) ^ n = -1
one_zpow: ∀ {α : Type ?u.1772} [inst : DivisionMonoid α] (n : ℤ), 1 ^ n = 1
one_zpow
α: Type u_1

inst✝: DivisionRing α

n: ℤ

h: Odd n

-1 = -1]
Goals accomplished! 🐙
#align odd.neg_one_zpow 
Odd.neg_one_zpow: ∀ {α : Type u_1} [inst : DivisionRing α] {n : ℤ}, Odd n → (-1) ^ n = -1
Odd.neg_one_zpow

end DivisionRing