[STATEMENT]
lemma resultant_const[simp]:
  fixes a :: "'a :: comm_ring_1"
  shows "resultant [:a:] q = a ^ (degree q)"
    and "resultant p [:a:] = a ^ (degree p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. resultant [:a:] q = a ^ degree q &&& resultant p [:a:] = a ^ degree p
[PROOF STEP]
unfolding resultant_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (sylvester_mat [:a:] q) = a ^ degree q &&& det (sylvester_mat p [:a:]) = a ^ degree p
[PROOF STEP]
unfolding sylvester_mat_const
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (a \<cdot>\<^sub>m 1\<^sub>m (degree q)) = a ^ degree q &&& det (a \<cdot>\<^sub>m 1\<^sub>m (degree p)) = a ^ degree p
[PROOF STEP]
by simp_all