case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
⊢ (fun x => eval x p) k ∈ σ (↑(aeval a) p)
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
⊢ (fun x => eval x p) '' σ a ⊆ σ (↑(aeval a) p)
rintro _ ⟨k, hk, rfl⟩
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
⊢ (fun x => eval x p) k ∈ σ (↑(aeval a) p)
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
⊢ (fun x => eval x p) k ∈ σ (↑(aeval a) p)
let q := C (eval k p) - p
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
hroot : IsRoot q k
⊢ (fun x => eval x p) k ∈ σ (↑(aeval a) p)
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
⊢ (fun x => eval x p) k ∈ σ (↑(aeval a) p)
have hroot : IsRoot q k := by simp only [eval_C, eval_sub, sub_self, IsRoot.def]
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
hroot✝ : (X - ↑C k) * (q / (X - ↑C k)) = q
hroot : (↑C k - X) * -(q / (X - ↑C k)) = q
⊢ (fun x => eval x p) k ∈ σ (↑(aeval a) p)
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
hroot : IsRoot q k
⊢ (fun x => eval x p) k ∈ σ (↑(aeval a) p)
rw [← mul_div_eq_iff_isRoot, ← neg_mul_neg, neg_sub] at hroot
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
hroot✝ : (X - ↑C k) * (q / (X - ↑C k)) = q
hroot : (↑C k - X) * -(q / (X - ↑C k)) = q
aeval_q_eq : ↑↑ₐ (eval k p) - ↑(aeval a) p = ↑(aeval a) q
⊢ (fun x => eval x p) k ∈ σ (↑(aeval a) p)
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
hroot✝ : (X - ↑C k) * (q / (X - ↑C k)) = q
hroot : (↑C k - X) * -(q / (X - ↑C k)) = q
⊢ (fun x => eval x p) k ∈ σ (↑(aeval a) p)
have aeval_q_eq : ↑ₐ (eval k p) - aeval a p = aeval a q := by
  simp only [aeval_C, AlgHom.map_sub, sub_left_inj]
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
hroot✝ : (X - ↑C k) * (q / (X - ↑C k)) = q
hroot : (↑C k - X) * -(q / (X - ↑C k)) = q
aeval_q_eq : ↑↑ₐ (eval k p) - ↑(aeval a) p = ↑(aeval a) q
⊢ ¬IsUnit (↑(aeval a) (↑C k - X) * ↑(aeval a) (-(q / (X - ↑C k))))
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
hroot✝ : (X - ↑C k) * (q / (X - ↑C k)) = q
hroot : (↑C k - X) * -(q / (X - ↑C k)) = q
aeval_q_eq : ↑↑ₐ (eval k p) - ↑(aeval a) p = ↑(aeval a) q
⊢ (fun x => eval x p) k ∈ σ (↑(aeval a) p)
rw [mem_iff, aeval_q_eq, ← hroot, aeval_mul]
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
hroot✝ : (X - ↑C k) * (q / (X - ↑C k)) = q
hroot : (↑C k - X) * -(q / (X - ↑C k)) = q
aeval_q_eq : ↑↑ₐ (eval k p) - ↑(aeval a) p = ↑(aeval a) q
hcomm : Commute (↑(aeval a) (↑C k - X)) (↑(aeval a) (-(q / (X - ↑C k))))
⊢ ¬IsUnit (↑(aeval a) (↑C k - X) * ↑(aeval a) (-(q / (X - ↑C k))))
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
hroot✝ : (X - ↑C k) * (q / (X - ↑C k)) = q
hroot : (↑C k - X) * -(q / (X - ↑C k)) = q
aeval_q_eq : ↑↑ₐ (eval k p) - ↑(aeval a) p = ↑(aeval a) q
⊢ ¬IsUnit (↑(aeval a) (↑C k - X) * ↑(aeval a) (-(q / (X - ↑C k))))
have hcomm := (Commute.all (C k - X) (-(q / (X - C k)))).map (aeval a : 𝕜[X] →ₐ[𝕜] A)
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
hroot✝ : (X - ↑C k) * (q / (X - ↑C k)) = q
hroot : (↑C k - X) * -(q / (X - ↑C k)) = q
aeval_q_eq : ↑↑ₐ (eval k p) - ↑(aeval a) p = ↑(aeval a) q
hcomm : Commute (↑(aeval a) (↑C k - X)) (↑(aeval a) (-(q / (X - ↑C k))))
⊢ ¬IsUnit (↑(aeval a) (↑C k - X))
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
hroot✝ : (X - ↑C k) * (q / (X - ↑C k)) = q
hroot : (↑C k - X) * -(q / (X - ↑C k)) = q
aeval_q_eq : ↑↑ₐ (eval k p) - ↑(aeval a) p = ↑(aeval a) q
hcomm : Commute (↑(aeval a) (↑C k - X)) (↑(aeval a) (-(q / (X - ↑C k))))
⊢ ¬IsUnit (↑(aeval a) (↑C k - X) * ↑(aeval a) (-(q / (X - ↑C k))))
apply mt fun h => (hcomm.isUnit_mul_iff.mp h).1
no goals
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
hroot✝ : (X - ↑C k) * (q / (X - ↑C k)) = q
hroot : (↑C k - X) * -(q / (X - ↑C k)) = q
aeval_q_eq : ↑↑ₐ (eval k p) - ↑(aeval a) p = ↑(aeval a) q
hcomm : Commute (↑(aeval a) (↑C k - X)) (↑(aeval a) (-(q / (X - ↑C k))))
⊢ ¬IsUnit (↑(aeval a) (↑C k - X))
simpa only [aeval_X, aeval_C, AlgHom.map_sub] using hk
no goals
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
⊢ IsRoot q k
simp only [eval_C, eval_sub, sub_self, IsRoot.def]
no goals
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
hroot✝ : (X - ↑C k) * (q / (X - ↑C k)) = q
hroot : (↑C k - X) * -(q / (X - ↑C k)) = q
⊢ ↑↑ₐ (eval k p) - ↑(aeval a) p = ↑(aeval a) q
simp only [aeval_C, AlgHom.map_sub, sub_left_inj]