let F be Field; :: thesis: for a being Element of F
for n being Nat holds multiplicity (((X- a) `^ n),a) = n
let a be Element of F; :: thesis: for n being Nat holds multiplicity (((X- a) `^ n),a) = n
let n be Nat; :: thesis: multiplicity (((X- a) `^ n),a) = n
set p = (X- a) `^ n;
set m = multiplicity (((X- a) `^ n),a);
I: n + 0 < n + 1 by XREAL_1:6;
(1_. F) *' ((X- a) `^ n) = (X- a) `^ n ;
then A: (X- a) `^ n divides (X- a) `^ n by RING_4:1;
( deg ((X- a) `^ (n + 1)) = n + 1 & deg ((X- a) `^ n) = n ) by Lm12a;
hence multiplicity (((X- a) `^ n),a) = n by A, I, RING_5:13, FIELD_14:67; :: thesis: verum