let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; for p being Polynomial of L
for z being Element of L st p <> 0_. L & z is_a_root_of p holds
deg (p div (rpoly (1,z))) = (deg p) - 1
let p be Polynomial of L; for z being Element of L st p <> 0_. L & z is_a_root_of p holds
deg (p div (rpoly (1,z))) = (deg p) - 1
let z be Element of L; ( p <> 0_. L & z is_a_root_of p implies deg (p div (rpoly (1,z))) = (deg p) - 1 )
assume that
A1:
p <> 0_. L
and
A2:
z is_a_root_of p
; deg (p div (rpoly (1,z))) = (deg p) - 1
consider s being Polynomial of L such that
A3:
p = (rpoly (1,z)) *' s
by A2, Th33;
A4:
rpoly (1,z) <> 0_. L
by A1, A3, POLYNOM4:2;
A5:
ex t being Polynomial of L st
( p = (s *' (rpoly (1,z))) + t & deg t < deg (rpoly (1,z)) )
s <> 0_. L
by A1, A3, POLYNOM3:34;
then deg p =
(deg (rpoly (1,z))) + (deg s)
by A3, A4, Th23
.=
1 + (deg s)
by Th27
;
hence
deg (p div (rpoly (1,z))) = (deg p) - 1
by A4, A5, Def5; verum