Theorem: RuesRotationallySymmetric (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
n : ℕ+
z rou : ℂ
h : rou ^ ↑n = 1
⊢ Rues n z = Rues n (z * rou)
Tactic:
simp_rw [Rues]
State after:
n : ℕ+
z rou : ℂ
h : rou ^ ↑n = 1
⊢ ∑' (k : ℕ), z ^ (↑n * k) / ↑(↑n * k).factorial = ∑' (k : ℕ), (z * rou) ^ (↑n * k) / ↑(↑n * k).factorial

State before:
n : ℕ+
z rou : ℂ
h : rou ^ ↑n = 1
⊢ ∑' (k : ℕ), z ^ (↑n * k) / ↑(↑n * k).factorial = ∑' (k : ℕ), (z * rou) ^ (↑n * k) / ↑(↑n * k).factorial
Tactic:
congr
State after:
case e_f
n : ℕ+
z rou : ℂ
h : rou ^ ↑n = 1
⊢ (fun k => z ^ (↑n * k) / ↑(↑n * k).factorial) = fun k => (z * rou) ^ (↑n * k) / ↑(↑n * k).factorial

State before:
case e_f
n : ℕ+
z rou : ℂ
h : rou ^ ↑n = 1
⊢ (fun k => z ^ (↑n * k) / ↑(↑n * k).factorial) = fun k => (z * rou) ^ (↑n * k) / ↑(↑n * k).factorial
Tactic:
ext1 k
State after:
case e_f.h
n : ℕ+
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
⊢ z ^ (↑n * k) / ↑(↑n * k).factorial = (z * rou) ^ (↑n * k) / ↑(↑n * k).factorial

State before:
case e_f.h
n : ℕ+
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
⊢ z ^ (↑n * k) / ↑(↑n * k).factorial = (z * rou) ^ (↑n * k) / ↑(↑n * k).factorial
Tactic:
have h₀ : (z * rou) ^ (n * k) = z ^ (n * k) * rou ^ (n * k) := by
  exact mul_pow z rou (↑n * k)
State after:
case e_f.h
n : ℕ+
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀ : (z * rou) ^ (↑n * k) = z ^ (↑n * k) * rou ^ (↑n * k)
⊢ z ^ (↑n * k) / ↑(↑n * k).factorial = (z * rou) ^ (↑n * k) / ↑(↑n * k).factorial

State before:
case e_f.h
n : ℕ+
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀ : (z * rou) ^ (↑n * k) = z ^ (↑n * k) * rou ^ (↑n * k)
⊢ z ^ (↑n * k) / ↑(↑n * k).factorial = (z * rou) ^ (↑n * k) / ↑(↑n * k).factorial
Tactic:
have h₁ : rou ^ (n * k) = (rou ^ (n : ℕ)) ^ k := by
  exact pow_mul rou (↑n) k
State after:
case e_f.h
n : ℕ+
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀ : (z * rou) ^ (↑n * k) = z ^ (↑n * k) * rou ^ (↑n * k)
h₁ : rou ^ (↑n * k) = (rou ^ ↑n) ^ k
⊢ z ^ (↑n * k) / ↑(↑n * k).factorial = (z * rou) ^ (↑n * k) / ↑(↑n * k).factorial

State before:
case e_f.h
n : ℕ+
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀ : (z * rou) ^ (↑n * k) = z ^ (↑n * k) * rou ^ (↑n * k)
h₁ : rou ^ (↑n * k) = (rou ^ ↑n) ^ k
⊢ z ^ (↑n * k) / ↑(↑n * k).factorial = (z * rou) ^ (↑n * k) / ↑(↑n * k).factorial
Tactic:
simp only [h₀, h₁, h, one_pow, mul_one]
State after:
no goals

State before:
n : ℕ+
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
⊢ (z * rou) ^ (↑n * k) = z ^ (↑n * k) * rou ^ (↑n * k)
Tactic:
exact mul_pow z rou (↑n * k)
State after:
no goals

State before:
n : ℕ+
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀ : (z * rou) ^ (↑n * k) = z ^ (↑n * k) * rou ^ (↑n * k)
⊢ rou ^ (↑n * k) = (rou ^ ↑n) ^ k
Tactic:
exact pow_mul rou (↑n) k
State after:
no goals