internlm/Lean-Github huggingface dataset:
Theorem: IsSeparable_of_isLocalization
Proof state before:
case intro.intro.intro.intro.refine_2.convert_6
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
P : Rₚ[X] := (Polynomial.map (algebraMap R Rₚ) (minpoly R x)).scaleRoots (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
⊢ eval₂ (algebraMap Rₚ Sₚ) ((algebraMap S Sₚ) x) (Polynomial.map (algebraMap R Rₚ) (minpoly R x)) = 0
Tactic:
rw [← aeval_def, ← map_aeval_eq_aeval_map, minpoly.aeval, map_zero]
Proof state after:
case intro.intro.intro.intro.refine_2.convert_6.h
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
P : Rₚ[X] := (Polynomial.map (algebraMap R Rₚ) (minpoly R x)).scaleRoots (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
⊢ (algebraMap Rₚ Sₚ).comp (algebraMap R Rₚ) = (algebraMap S Sₚ).comp (algebraMap R S)
Theorem: IsSeparable_of_isLocalization
Proof state before:
case intro.intro.intro.intro.refine_2.convert_6.h
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
P : Rₚ[X] := (Polynomial.map (algebraMap R Rₚ) (minpoly R x)).scaleRoots (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
⊢ (algebraMap Rₚ Sₚ).comp (algebraMap R Rₚ) = (algebraMap S Sₚ).comp (algebraMap R S)
Tactic:
rw [← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
Proof state after:
no goals
Theorem: Algebra.isNilpotent_trace_of_isNilpotent
Proof state before:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
⊢ IsNilpotent ((trace R S) x)
Tactic:
by_cases hS : ∃ s : Finset S, Nonempty (Basis s R S)
Proof state after:
case pos
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
hS : ∃ s, Nonempty (Basis { x // x ∈ s } R S)
⊢ IsNilpotent ((trace R S) x)

case neg
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
hS : ¬∃ s, Nonempty (Basis { x // x ∈ s } R S)
⊢ IsNilpotent ((trace R S) x)
Theorem: Algebra.isNilpotent_trace_of_isNilpotent
Proof state before:
case pos
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
hS : ∃ s, Nonempty (Basis { x // x ∈ s } R S)
⊢ IsNilpotent ((trace R S) x)
Tactic:
obtain ⟨s, ⟨b⟩⟩ := hS
Proof state after:
case pos.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
s : Finset S
b : Basis { x // x ∈ s } R S
⊢ IsNilpotent ((trace R S) x)
Theorem: Algebra.isNilpotent_trace_of_isNilpotent
Proof state before:
case pos.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
s : Finset S
b : Basis { x // x ∈ s } R S
⊢ IsNilpotent ((trace R S) x)
Tactic:
have := Module.Finite.of_basis b
Proof state after:
case pos.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
s : Finset S
b : Basis { x // x ∈ s } R S
this : Module.Finite R S
⊢ IsNilpotent ((trace R S) x)
Theorem: Algebra.isNilpotent_trace_of_isNilpotent
Proof state before:
case pos.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
s : Finset S
b : Basis { x // x ∈ s } R S
this : Module.Finite R S
⊢ IsNilpotent ((trace R S) x)
Tactic:
have := (Module.free_def.{u, v, v} R S).mpr ⟨s, ⟨b⟩⟩
Proof state after:
case pos.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
s : Finset S
b : Basis { x // x ∈ s } R S
this✝ : Module.Finite R S
this : Module.Free R S
⊢ IsNilpotent ((trace R S) x)
Theorem: Algebra.isNilpotent_trace_of_isNilpotent
Proof state before:
case pos.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
s : Finset S
b : Basis { x // x ∈ s } R S
this✝ : Module.Finite R S
this : Module.Free R S
⊢ IsNilpotent ((trace R S) x)
Tactic:
apply LinearMap.isNilpotent_trace_of_isNilpotent (hx.map (lmul R S))
Proof state after:
no goals
Theorem: Algebra.isNilpotent_trace_of_isNilpotent
Proof state before:
case neg
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
hS : ¬∃ s, Nonempty (Basis { x // x ∈ s } R S)
⊢ IsNilpotent ((trace R S) x)
Tactic:
rw [trace_eq_zero_of_not_exists_basis _ hS, LinearMap.zero_apply]
Proof state after:
case neg
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
hS : ¬∃ s, Nonempty (Basis { x // x ∈ s } R S)
⊢ IsNilpotent 0
Theorem: Algebra.isNilpotent_trace_of_isNilpotent
Proof state before:
case neg
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
hS : ¬∃ s, Nonempty (Basis { x // x ∈ s } R S)
⊢ IsNilpotent 0
Tactic:
exact IsNilpotent.zero
Proof state after:
no goals
Theorem: FiniteDimensional.finrank_le_of_span_eq_top
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
ι : Type u_3
inst✝ : Fintype ι
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
⊢ finrank R M ≤ Fintype.card ι
Tactic:
classical
rw [← finrank_top, ← hv]
exact (finrank_span_le_card _).trans (by convert Fintype.card_range_le v; rw [Set.toFinset_card])
Proof state after:
no goals
Theorem: FiniteDimensional.finrank_le_of_span_eq_top
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
ι : Type u_3
inst✝ : Fintype ι
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
⊢ finrank R M ≤ Fintype.card ι
Tactic:
rw [← finrank_top, ← hv]
Proof state after:
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
ι : Type u_3
inst✝ : Fintype ι
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
⊢ finrank R ↥(Submodule.span R (Set.range v)) ≤ Fintype.card ι
Theorem: FiniteDimensional.finrank_le_of_span_eq_top
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
ι : Type u_3
inst✝ : Fintype ι
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
⊢ finrank R ↥(Submodule.span R (Set.range v)) ≤ Fintype.card ι
Tactic:
exact (finrank_span_le_card _).trans (by convert Fintype.card_range_le v; rw [Set.toFinset_card])
Proof state after:
no goals
Theorem: FiniteDimensional.finrank_le_of_span_eq_top
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
ι : Type u_3
inst✝ : Fintype ι
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
⊢ (Set.range v).toFinset.card ≤ Fintype.card ι
Tactic:
convert Fintype.card_range_le v
Proof state after:
case h.e'_3
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
ι : Type u_3
inst✝ : Fintype ι
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
⊢ (Set.range v).toFinset.card = Fintype.card ↑(Set.range v)
Theorem: FiniteDimensional.finrank_le_of_span_eq_top
Proof state before:
case h.e'_3
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
ι : Type u_3
inst✝ : Fintype ι
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
⊢ (Set.range v).toFinset.card = Fintype.card ↑(Set.range v)
Tactic:
rw [Set.toFinset_card]
Proof state after:
no goals
Theorem: Polynomial.irreducible_taylor_iff
Proof state before:
R : Type u_1
inst✝ : CommRing R
r : R
p : R[X]
⊢ Irreducible ((taylor r) p) ↔ Irreducible p
Tactic:
refine ⟨fun H ↦ of_irreducible_map (taylorAlgEquiv r).toRingEquiv H, fun H ↦ ?_⟩
Proof state after:
R : Type u_1
inst✝ : CommRing R
r : R
p : R[X]
H : Irreducible p
⊢ Irreducible ((taylor r) p)
Theorem: Polynomial.irreducible_taylor_iff
Proof state before:
R : Type u_1
inst✝ : CommRing R
r : R
p : R[X]
H : Irreducible p
⊢ Irreducible ((taylor r) p)
Tactic:
apply of_irreducible_map ((taylorAlgEquiv r).symm.toRingEquiv : R[X] →+* R[X])
Proof state after:
R : Type u_1
inst✝ : CommRing R
r : R
p : R[X]
H : Irreducible p
⊢ Irreducible (↑(taylorAlgEquiv r).symm.toRingEquiv ((taylor r) p))
Theorem: Polynomial.irreducible_taylor_iff
Proof state before:
R : Type u_1
inst✝ : CommRing R
r : R
p : R[X]
H : Irreducible p
⊢ Irreducible (↑(taylorAlgEquiv r).symm.toRingEquiv ((taylor r) p))
Tactic:
simpa only [AlgEquiv.toRingEquiv_eq_coe, RingHom.coe_coe, AlgEquiv.coe_ringEquiv,
  taylorAlgEquiv_symm_apply, taylor_taylor, add_left_neg, taylor_zero', LinearMap.id_coe, id_eq]
Proof state after:
no goals
Theorem: Polynomial.separable_map'
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
p : R[X]
⊢ (map f p).Separable ↔ p.Separable
Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ H.map⟩
Proof state after:
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
p : R[X]
H : (map f p).Separable
⊢ p.Separable
Theorem: Polynomial.separable_map'
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
p : R[X]
H : (map f p).Separable
⊢ p.Separable
Tactic:
obtain ⟨m, hm⟩ := Ideal.exists_maximal S
Proof state after:
case intro
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
p : R[X]
H : (map f p).Separable
m : Ideal S
hm : m.IsMaximal
⊢ p.Separable
Theorem: Polynomial.separable_map'
Proof state before:
case intro
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
p : R[X]
H : (map f p).Separable
m : Ideal S
hm : m.IsMaximal
⊢ p.Separable
Tactic:
have := Separable.map H (f := Ideal.Quotient.mk m)
Proof state after:
case intro
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
p : R[X]
H : (map f p).Separable
m : Ideal S
hm : m.IsMaximal
this : (map (Ideal.Quotient.mk m) (map f p)).Separable
⊢ p.Separable
Theorem: Polynomial.separable_map'
Proof state before:
case intro
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
p : R[X]
H : (map f p).Separable
m : Ideal S
hm : m.IsMaximal
this : (map (Ideal.Quotient.mk m) (map f p)).Separable
⊢ p.Separable
Tactic:
rwa [map_map, separable_map] at this
Proof state after:
no goals
Theorem: Polynomial.dvd_C_mul_X_sub_one_pow_add_one
Proof state before:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : p.Prime
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
⊢ C r ∣ (C a * X - 1) ^ p + 1
Tactic:
rw [sub_eq_add_neg, add_pow_prime_eq hpri, (hpri.odd_of_ne_two hp).neg_pow, one_pow,
  mul_pow, ← C.map_pow, add_comm, add_comm (_ * _), ← add_assoc, ← add_assoc,
  add_right_neg, zero_add]
Proof state after:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : p.Prime
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
⊢ C r ∣ C (a ^ p) * X ^ p + ↑p * ∑ k ∈ Finset.Ioo 0 p, (C a * X) ^ k * (-1) ^ (p - k) * ↑(p.choose k / p)
Theorem: Polynomial.dvd_C_mul_X_sub_one_pow_add_one
Proof state before:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : p.Prime
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
⊢ C r ∣ C (a ^ p) * X ^ p + ↑p * ∑ k ∈ Finset.Ioo 0 p, (C a * X) ^ k * (-1) ^ (p - k) * ↑(p.choose k / p)
Tactic:
refine dvd_add (dvd_mul_of_dvd_left (_root_.map_dvd C h₁) _) ((_root_.map_dvd C h₂).trans ?_)
Proof state after:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : p.Prime
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
⊢ C (↑p * a) ∣ ↑p * ∑ k ∈ Finset.Ioo 0 p, (C a * X) ^ k * (-1) ^ (p - k) * ↑(p.choose k / p)
Theorem: Polynomial.dvd_C_mul_X_sub_one_pow_add_one
Proof state before:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : p.Prime
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
⊢ C (↑p * a) ∣ ↑p * ∑ k ∈ Finset.Ioo 0 p, (C a * X) ^ k * (-1) ^ (p - k) * ↑(p.choose k / p)
Tactic:
rw [map_mul, map_natCast]
Proof state after:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : p.Prime
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
⊢ ↑p * C a ∣ ↑p * ∑ k ∈ Finset.Ioo 0 p, (C a * X) ^ k * (-1) ^ (p - k) * ↑(p.choose k / p)
Theorem: Polynomial.dvd_C_mul_X_sub_one_pow_add_one
Proof state before:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : p.Prime
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
⊢ ↑p * C a ∣ ↑p * ∑ k ∈ Finset.Ioo 0 p, (C a * X) ^ k * (-1) ^ (p - k) * ↑(p.choose k / p)
Tactic:
exact mul_dvd_mul_left _ (Finset.dvd_sum (fun x hx ↦ dvd_mul_of_dvd_left
  (dvd_mul_of_dvd_left (dvd_pow (dvd_mul_right _ _) (Finset.mem_Ioo.mp hx).1.ne.symm) _) _))
Proof state after:
no goals
Theorem: pow_sub_pow_eq_prod_sub_zeta_runity_mul
Proof 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
Proof 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)
Theorem: pow_sub_pow_eq_prod_sub_zeta_runity_mul
Proof 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
Proof 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)
Theorem: pow_sub_pow_eq_prod_sub_zeta_runity_mul
Proof 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
Proof 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)
Theorem: pow_sub_pow_eq_prod_sub_zeta_runity_mul
Proof 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
Proof 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)
Theorem: pow_sub_pow_eq_prod_sub_zeta_runity_mul
Proof 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
Proof 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)
Theorem: pow_sub_pow_eq_prod_sub_zeta_runity_mul
Proof 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]
Proof state after:
no goals
Theorem: pow_sub_pow_eq_prod_sub_zeta_runity_mul
Proof 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
Proof 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)
Theorem: pow_sub_pow_eq_prod_sub_zeta_runity_mul
Proof 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
Proof state after:
no goals
Theorem: pow_add_pow_eq_prod_add_zeta_runity_mul
Proof 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)
Proof 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)
Theorem: pow_add_pow_eq_prod_add_zeta_runity_mul
Proof 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
Proof 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)
Theorem: pow_add_pow_eq_prod_add_zeta_runity_mul
Proof 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
Proof 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)
Theorem: pow_add_pow_eq_prod_add_zeta_runity_mul
Proof 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
Proof state after:
no goals