𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : Set.Nonempty (σ a)
✝ : Nontrivial A
⊢ σ (↑(aeval a) p) = (fun k => eval k p) '' σ a
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : Set.Nonempty (σ a)
⊢ σ (↑(aeval a) p) = (fun k => eval k p) '' σ a
nontriviality A
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : Set.Nonempty (σ a)
✝ : Nontrivial A
h : degree p ≤ 0
⊢ σ (↑(aeval a) p) = (fun k => eval k p) '' σ a
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : Set.Nonempty (σ a)
✝ : Nontrivial A
⊢ σ (↑(aeval a) p) = (fun k => eval k p) '' σ a
refine' Or.elim (le_or_gt (degree p) 0) (fun h => _) (map_polynomial_aeval_of_degree_pos a p)
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : Set.Nonempty (σ a)
✝ : Nontrivial A
h : degree p ≤ 0
⊢ σ (↑(aeval a) (↑C (coeff p 0))) = (fun k => eval k (↑C (coeff p 0))) '' σ a
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : Set.Nonempty (σ a)
✝ : Nontrivial A
h : degree p ≤ 0
⊢ σ (↑(aeval a) p) = (fun k => eval k p) '' σ a
rw [eq_C_of_degree_le_zero h]
no goals
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : Set.Nonempty (σ a)
✝ : Nontrivial A
h : degree p ≤ 0
⊢ σ (↑(aeval a) (↑C (coeff p 0))) = (fun k => eval k (↑C (coeff p 0))) '' σ a
simp only [Set.image_congr, eval_C, aeval_C, scalar_eq, Set.Nonempty.image_const hnon]