[STATEMENT]
lemma factor_theorem:
  assumes "f \<in> carrier P"
  assumes "a \<in> carrier R"
  assumes "g = UP_root_div f a"
  assumes "to_fun f a = \<zero>"
  shows "f = (X_minus a) \<otimes>\<^bsub>P\<^esub> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = X_poly_minus R a \<otimes>\<^bsub>P\<^esub> g
[PROOF STEP]
using remainder_theorem[of f a g _] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>f \<in> carrier P; a \<in> carrier R; g = UP_root_div f a; ?r = UP_root_rem f a\<rbrakk> \<Longrightarrow> f = ?r \<oplus>\<^bsub>P\<^esub> X_poly_minus R a \<otimes>\<^bsub>P\<^esub> g
f \<in> carrier P
a \<in> carrier R
g = UP_root_div f a
to_fun f a = \<zero>

goal (1 subgoal):
 1. f = X_poly_minus R a \<otimes>\<^bsub>P\<^esub> g
[PROOF STEP]
unfolding UP_root_rem_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>f \<in> carrier P; a \<in> carrier R; g = UP_root_div f a; ?r = monom P (T\<^bsub>a\<^esub> f 0) 0\<rbrakk> \<Longrightarrow> f = ?r \<oplus>\<^bsub>P\<^esub> X_poly_minus R a \<otimes>\<^bsub>P\<^esub> g
f \<in> carrier P
a \<in> carrier R
g = UP_root_div f a
to_fun f a = \<zero>

goal (1 subgoal):
 1. f = X_poly_minus R a \<otimes>\<^bsub>P\<^esub> g
[PROOF STEP]
by (simp add: ctrm_zcf taylor_zcf taylor_closed UP_root_div_closed X_minus_closed)