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

State before:
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
x y : K
⊢ x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n K, (x - ζ * y)
Tactic:
suffices
  (X 0 : MvPolynomial (Fin 2) K) ^ (n : ℕ) - X 1 ^ (n : ℕ) =
    ∏ ζ in nthRootsFinset n K, (X 0 - MvPolynomial.C ζ * X 1)
  by
  apply_fun MvPolynomial.eval fun i : Fin 2 => if i = 0 then x else y at this
  simpa [MvPolynomial.eval_prod] using this
State after:
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
x y : K
⊢ MvPolynomial.X 0 ^ n - MvPolynomial.X 1 ^ n =
    ∏ ζ ∈ nthRootsFinset n K, (MvPolynomial.X 0 - MvPolynomial.C ζ * MvPolynomial.X 1)

State before:
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
x y : K
⊢ MvPolynomial.X 0 ^ n - MvPolynomial.X 1 ^ n =
    ∏ ζ ∈ nthRootsFinset n K, (MvPolynomial.X 0 - MvPolynomial.C ζ * MvPolynomial.X 1)
Tactic:
have := X_pow_sub_one_eq_prod hpos h
State after:
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
x y : K
this : Polynomial.X ^ n - 1 = ∏ ζ ∈ nthRootsFinset n K, (Polynomial.X - Polynomial.C ζ)
⊢ MvPolynomial.X 0 ^ n - MvPolynomial.X 1 ^ n =
    ∏ ζ ∈ nthRootsFinset n K, (MvPolynomial.X 0 - MvPolynomial.C ζ * MvPolynomial.X 1)

State before:
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
x y : K
this : Polynomial.X ^ n - 1 = ∏ ζ ∈ nthRootsFinset n K, (Polynomial.X - Polynomial.C ζ)
⊢ MvPolynomial.X 0 ^ n - MvPolynomial.X 1 ^ n =
    ∏ ζ ∈ nthRootsFinset n K, (MvPolynomial.X 0 - MvPolynomial.C ζ * MvPolynomial.X 1)
Tactic:
have := congr_arg (Polynomial.aeval (X 0 : MvPolynomial (Fin 2) K)) this
State after:
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
x y : K
this✝ : Polynomial.X ^ n - 1 = ∏ ζ ∈ nthRootsFinset n K, (Polynomial.X - Polynomial.C ζ)
this :
  (Polynomial.aeval (MvPolynomial.X 0)) (Polynomial.X ^ n - 1) =
    (Polynomial.aeval (MvPolynomial.X 0)) (∏ ζ ∈ nthRootsFinset n K, (Polynomial.X - Polynomial.C ζ))
⊢ MvPolynomial.X 0 ^ n - MvPolynomial.X 1 ^ n =
    ∏ ζ ∈ nthRootsFinset n K, (MvPolynomial.X 0 - MvPolynomial.C ζ * MvPolynomial.X 1)

State before:
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
x y : K
this✝ : Polynomial.X ^ n - 1 = ∏ ζ ∈ nthRootsFinset n K, (Polynomial.X - Polynomial.C ζ)
this :
  (Polynomial.aeval (MvPolynomial.X 0)) (Polynomial.X ^ n - 1) =
    (Polynomial.aeval (MvPolynomial.X 0)) (∏ ζ ∈ nthRootsFinset n K, (Polynomial.X - Polynomial.C ζ))
⊢ MvPolynomial.X 0 ^ n - MvPolynomial.X 1 ^ n =
    ∏ ζ ∈ nthRootsFinset n K, (MvPolynomial.X 0 - MvPolynomial.C ζ * MvPolynomial.X 1)
Tactic:
simp only [map_prod, aeval_X_pow, Polynomial.aeval_X, aeval_one, Polynomial.aeval_C,
  AlgHom.map_sub] at this
State after:
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
x y : K
this✝ : Polynomial.X ^ n - 1 = ∏ ζ ∈ nthRootsFinset n K, (Polynomial.X - Polynomial.C ζ)
this :
  MvPolynomial.X 0 ^ n - 1 = ∏ x ∈ nthRootsFinset n K, (MvPolynomial.X 0 - (algebraMap K (MvPolynomial (Fin 2) K)) x)
⊢ MvPolynomial.X 0 ^ n - MvPolynomial.X 1 ^ n =
    ∏ ζ ∈ nthRootsFinset n K, (MvPolynomial.X 0 - MvPolynomial.C ζ * MvPolynomial.X 1)

State before:
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
x y : K
this✝ : Polynomial.X ^ n - 1 = ∏ ζ ∈ nthRootsFinset n K, (Polynomial.X - Polynomial.C ζ)
this :
  MvPolynomial.X 0 ^ n - 1 = ∏ x ∈ nthRootsFinset n K, (MvPolynomial.X 0 - (algebraMap K (MvPolynomial (Fin 2) K)) x)
⊢ MvPolynomial.X 0 ^ n - MvPolynomial.X 1 ^ n =
    ∏ ζ ∈ nthRootsFinset n K, (MvPolynomial.X 0 - MvPolynomial.C ζ * MvPolynomial.X 1)
Tactic:
have := congr_arg (homogenization 1) this
State after:
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
x y : K
this✝¹ : Polynomial.X ^ n - 1 = ∏ ζ ∈ nthRootsFinset n K, (Polynomial.X - Polynomial.C ζ)
this✝ :
  MvPolynomial.X 0 ^ n - 1 = ∏ x ∈ nthRootsFinset n K, (MvPolynomial.X 0 - (algebraMap K (MvPolynomial (Fin 2) K)) x)
this :
  homogenization 1 (MvPolynomial.X 0 ^ n - 1) =
    homogenization 1 (∏ x ∈ nthRootsFinset n K, (MvPolynomial.X 0 - (algebraMap K (MvPolynomial (Fin 2) K)) x))
⊢ MvPolynomial.X 0 ^ n - MvPolynomial.X 1 ^ n =
    ∏ ζ ∈ nthRootsFinset n K, (MvPolynomial.X 0 - MvPolynomial.C ζ * MvPolynomial.X 1)

State before:
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
x y : K
this✝¹ : Polynomial.X ^ n - 1 = ∏ ζ ∈ nthRootsFinset n K, (Polynomial.X - Polynomial.C ζ)
this✝ :
  MvPolynomial.X 0 ^ n - 1 = ∏ x ∈ nthRootsFinset n K, (MvPolynomial.X 0 - (algebraMap K (MvPolynomial (Fin 2) K)) x)
this :
  homogenization 1 (MvPolynomial.X 0 ^ n - 1) =
    homogenization 1 (∏ x ∈ nthRootsFinset n K, (MvPolynomial.X 0 - (algebraMap K (MvPolynomial (Fin 2) K)) x))
⊢ MvPolynomial.X 0 ^ n - MvPolynomial.X 1 ^ n =
    ∏ ζ ∈ nthRootsFinset n K, (MvPolynomial.X 0 - MvPolynomial.C ζ * MvPolynomial.X 1)
Tactic:
simpa [homogenization_prod, Polynomial.algebraMap_eq, hpos]
State after:
no goals

State before:
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
x y : K
this :
  MvPolynomial.X 0 ^ n - MvPolynomial.X 1 ^ n =
    ∏ ζ ∈ nthRootsFinset n K, (MvPolynomial.X 0 - MvPolynomial.C ζ * MvPolynomial.X 1)
⊢ x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n K, (x - ζ * y)
Tactic:
apply_fun MvPolynomial.eval fun i : Fin 2 => if i = 0 then x else y at this
State after:
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
x y : K
this :
  (MvPolynomial.eval fun i => if i = 0 then x else y) (MvPolynomial.X 0 ^ n - MvPolynomial.X 1 ^ n) =
    (MvPolynomial.eval fun i => if i = 0 then x else y)
      (∏ ζ ∈ nthRootsFinset n K, (MvPolynomial.X 0 - MvPolynomial.C ζ * MvPolynomial.X 1))
⊢ x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n K, (x - ζ * y)

State before:
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
x y : K
this :
  (MvPolynomial.eval fun i => if i = 0 then x else y) (MvPolynomial.X 0 ^ n - MvPolynomial.X 1 ^ n) =
    (MvPolynomial.eval fun i => if i = 0 then x else y)
      (∏ ζ ∈ nthRootsFinset n K, (MvPolynomial.X 0 - MvPolynomial.C ζ * MvPolynomial.X 1))
⊢ x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n K, (x - ζ * y)
Tactic:
simpa [MvPolynomial.eval_prod] using this
State after:
no goals