Theorem: zeta_runity_pow_even (FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean)

State before:
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hpo : Odd ↑p
n : ℕ
⊢ ∃ m, hζ.unit' ^ n = hζ.unit' ^ (2 * m)
Tactic:
rcases eq_or_ne n 0 with (rfl | _)
State after:
case inl
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hpo : Odd ↑p
⊢ ∃ m, hζ.unit' ^ 0 = hζ.unit' ^ (2 * m)

case inr
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hpo : Odd ↑p
n : ℕ
h✝ : n ≠ 0
⊢ ∃ m, hζ.unit' ^ n = hζ.unit' ^ (2 * m)

State before:
case inr
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hpo : Odd ↑p
n : ℕ
h✝ : n ≠ 0
⊢ ∃ m, hζ.unit' ^ n = hζ.unit' ^ (2 * m)
Tactic:
obtain ⟨r, hr⟩ := hpo
State after:
case inr.intro
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℕ
h✝ : n ≠ 0
r : ℕ
hr : ↑p = 2 * r + 1
⊢ ∃ m, hζ.unit' ^ n = hζ.unit' ^ (2 * m)

State before:
case inr.intro
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℕ
h✝ : n ≠ 0
r : ℕ
hr : ↑p = 2 * r + 1
⊢ ∃ m, hζ.unit' ^ n = hζ.unit' ^ (2 * m)
Tactic:
have he : 2 * (r + 1) * n = p * n + n := by rw [hr]; ring
State after:
case inr.intro
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℕ
h✝ : n ≠ 0
r : ℕ
hr : ↑p = 2 * r + 1
he : 2 * (r + 1) * n = ↑p * n + n
⊢ ∃ m, hζ.unit' ^ n = hζ.unit' ^ (2 * m)

State before:
case inr.intro
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℕ
h✝ : n ≠ 0
r : ℕ
hr : ↑p = 2 * r + 1
he : 2 * (r + 1) * n = ↑p * n + n
⊢ ∃ m, hζ.unit' ^ n = hζ.unit' ^ (2 * m)
Tactic:
use (r + 1) * n
State after:
case h
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℕ
h✝ : n ≠ 0
r : ℕ
hr : ↑p = 2 * r + 1
he : 2 * (r + 1) * n = ↑p * n + n
⊢ hζ.unit' ^ n = hζ.unit' ^ (2 * ((r + 1) * n))

State before:
case h
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℕ
h✝ : n ≠ 0
r : ℕ
hr : ↑p = 2 * r + 1
he : 2 * (r + 1) * n = ↑p * n + n
⊢ hζ.unit' ^ n = hζ.unit' ^ (2 * ((r + 1) * n))
Tactic:
rw [← mul_assoc, he, pow_add]
State after:
case h
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℕ
h✝ : n ≠ 0
r : ℕ
hr : ↑p = 2 * r + 1
he : 2 * (r + 1) * n = ↑p * n + n
⊢ hζ.unit' ^ n = hζ.unit' ^ (↑p * n) * hζ.unit' ^ n

State before:
case h
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℕ
h✝ : n ≠ 0
r : ℕ
hr : ↑p = 2 * r + 1
he : 2 * (r + 1) * n = ↑p * n + n
⊢ hζ.unit' ^ n = hζ.unit' ^ (↑p * n) * hζ.unit' ^ n
Tactic:
convert (one_mul (M := (𝓞 K)ˣ) _).symm
State after:
case h.e'_3.h.e'_5
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℕ
h✝ : n ≠ 0
r : ℕ
hr : ↑p = 2 * r + 1
he : 2 * (r + 1) * n = ↑p * n + n
⊢ hζ.unit' ^ (↑p * n) = 1

State before:
case h.e'_3.h.e'_5
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℕ
h✝ : n ≠ 0
r : ℕ
hr : ↑p = 2 * r + 1
he : 2 * (r + 1) * n = ↑p * n + n
⊢ hζ.unit' ^ (↑p * n) = 1
Tactic:
rw [pow_mul, hζ.unit'_pow, one_pow]
State after:
no goals

State before:
case inl
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hpo : Odd ↑p
⊢ ∃ m, hζ.unit' ^ 0 = hζ.unit' ^ (2 * m)
Tactic:
use 0
State after:
no goals

State before:
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℕ
h✝ : n ≠ 0
r : ℕ
hr : ↑p = 2 * r + 1
⊢ 2 * (r + 1) * n = ↑p * n + n
Tactic:
rw [hr]
State after:
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℕ
h✝ : n ≠ 0
r : ℕ
hr : ↑p = 2 * r + 1
⊢ 2 * (r + 1) * n = (2 * r + 1) * n + n

State before:
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℕ
h✝ : n ≠ 0
r : ℕ
hr : ↑p = 2 * r + 1
⊢ 2 * (r + 1) * n = (2 * r + 1) * n + n
Tactic:
ring
State after:
no goals