case intro
R : Type u_1
S : Type u_2
T : Type ?u.680661
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.680964
B : Type ?u.680967
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.681389
inst✝¹ : Field K
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
⊢ ↑(aeval x) f ∈ Submodule.span R (Set.range fun i => x ^ ↑i)
R : Type u_1
S : Type u_2
T : Type ?u.680661
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.680964
B : Type ?u.680967
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.681389
inst✝¹ : Field K
inst✝ : Nontrivial R
x y : S
hx : IsIntegral R x
hy : ∃ f, y = ↑(aeval x) f
⊢ y ∈ Submodule.span R (Set.range fun i => x ^ ↑i)
obtain ⟨f, rfl⟩ := hy
R : Type u_1
S : Type u_2
T : Type ?u.680661
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.680964
B : Type ?u.680967
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.681389
inst✝¹ : Field K
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
⊢ ∃ f_1, degree f_1 < ↑(natDegree (minpoly R x)) ∧ ↑(aeval x) f = ↑(aeval x) f_1
case intro
R : Type u_1
S : Type u_2
T : Type ?u.680661
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.680964
B : Type ?u.680967
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.681389
inst✝¹ : Field K
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
⊢ ↑(aeval x) f ∈ Submodule.span R (Set.range fun i => x ^ ↑i)
apply mem_span_pow'.mpr _
R : Type u_1
S : Type u_2
T : Type ?u.680661
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.680964
B : Type ?u.680967
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.681389
inst✝¹ : Field K
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : Monic (minpoly R x)
⊢ ∃ f_1, degree f_1 < ↑(natDegree (minpoly R x)) ∧ ↑(aeval x) f = ↑(aeval x) f_1
R : Type u_1
S : Type u_2
T : Type ?u.680661
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.680964
B : Type ?u.680967
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.681389
inst✝¹ : Field K
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
⊢ ∃ f_1, degree f_1 < ↑(natDegree (minpoly R x)) ∧ ↑(aeval x) f = ↑(aeval x) f_1
have := minpoly.monic hx
R : Type u_1
S : Type u_2
T : Type ?u.680661
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.680964
B : Type ?u.680967
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.681389
inst✝¹ : Field K
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : Monic (minpoly R x)
⊢ ↑(aeval x) f = ↑(aeval x) (f %ₘ minpoly R x)
R : Type u_1
S : Type u_2
T : Type ?u.680661
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.680964
B : Type ?u.680967
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.681389
inst✝¹ : Field K
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : Monic (minpoly R x)
⊢ ∃ f_1, degree f_1 < ↑(natDegree (minpoly R x)) ∧ ↑(aeval x) f = ↑(aeval x) f_1
refine' ⟨f %ₘ minpoly R x, (degree_modByMonic_lt _ this).trans_le degree_le_natDegree, _⟩
R : Type u_1
S : Type u_2
T : Type ?u.680661
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.680964
B : Type ?u.680967
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.681389
inst✝¹ : Field K
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : Monic (minpoly R x)
⊢ ↑(aeval x) (f %ₘ minpoly R x + minpoly R x * (f /ₘ minpoly R x)) = ↑(aeval x) (f %ₘ minpoly R x)
R : Type u_1
S : Type u_2
T : Type ?u.680661
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.680964
B : Type ?u.680967
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.681389
inst✝¹ : Field K
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : Monic (minpoly R x)
⊢ ↑(aeval x) f = ↑(aeval x) (f %ₘ minpoly R x)
conv_lhs => rw [← modByMonic_add_div f this]
no goals
R : Type u_1
S : Type u_2
T : Type ?u.680661
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.680964
B : Type ?u.680967
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.681389
inst✝¹ : Field K
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : Monic (minpoly R x)
⊢ ↑(aeval x) (f %ₘ minpoly R x + minpoly R x * (f /ₘ minpoly R x)) = ↑(aeval x) (f %ₘ minpoly R x)
simp only [add_zero, MulZeroClass.zero_mul, minpoly.aeval, aeval_add, AlgHom.map_mul]