rw [hr]
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
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