Theorem: pow_add_pow_eq_prod_add_zeta_runity_mul (FltRegular/NumberTheory/Cyclotomic/Factoring.lean)

State before:
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hodd : n % 2 = 1
h : IsPrimitiveRoot ζ n
x y : K
⊢ x ^ n + y ^ n = ∏ ζ ∈ nthRootsFinset n K, (x + ζ * y)
Tactic:
have := pow_sub_pow_eq_prod_sub_zeta_runity_mul (Nat.odd_iff.mpr hodd).pos h x (-y)
State after:
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hodd : n % 2 = 1
h : IsPrimitiveRoot ζ n
x y : K
this : x ^ n - (-y) ^ n = ∏ ζ ∈ nthRootsFinset n K, (x - ζ * -y)
⊢ x ^ n + y ^ n = ∏ ζ ∈ nthRootsFinset n K, (x + ζ * y)

State before:
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hodd : n % 2 = 1
h : IsPrimitiveRoot ζ n
x y : K
this : x ^ n - (-y) ^ n = ∏ ζ ∈ nthRootsFinset n K, (x - ζ * -y)
⊢ x ^ n + y ^ n = ∏ ζ ∈ nthRootsFinset n K, (x + ζ * y)
Tactic:
simp only [mul_neg, sub_neg_eq_add] at this
State after:
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hodd : n % 2 = 1
h : IsPrimitiveRoot ζ n
x y : K
this : x ^ n - (-y) ^ n = ∏ x_1 ∈ nthRootsFinset n K, (x + x_1 * y)
⊢ x ^ n + y ^ n = ∏ ζ ∈ nthRootsFinset n K, (x + ζ * y)

State before:
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hodd : n % 2 = 1
h : IsPrimitiveRoot ζ n
x y : K
this : x ^ n - (-y) ^ n = ∏ x_1 ∈ nthRootsFinset n K, (x + x_1 * y)
⊢ x ^ n + y ^ n = ∏ ζ ∈ nthRootsFinset n K, (x + ζ * y)
Tactic:
rw [neg_pow, neg_one_pow_eq_pow_mod_two] at this
State after:
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hodd : n % 2 = 1
h : IsPrimitiveRoot ζ n
x y : K
this : x ^ n - (-1) ^ (n % 2) * y ^ n = ∏ x_1 ∈ nthRootsFinset n K, (x + x_1 * y)
⊢ x ^ n + y ^ n = ∏ ζ ∈ nthRootsFinset n K, (x + ζ * y)

State before:
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hodd : n % 2 = 1
h : IsPrimitiveRoot ζ n
x y : K
this : x ^ n - (-1) ^ (n % 2) * y ^ n = ∏ x_1 ∈ nthRootsFinset n K, (x + x_1 * y)
⊢ x ^ n + y ^ n = ∏ ζ ∈ nthRootsFinset n K, (x + ζ * y)
Tactic:
simpa [hodd] using this
State after:
no goals