let R be algebraic-closed Field; for p being Element of the carrier of (Polynom-Ring R) holds
( p is irreducible iff deg p = 1 )
let p be Element of the carrier of (Polynom-Ring R); ( p is irreducible iff deg p = 1 )
set K = Polynom-Ring R;
now ( p is irreducible implies deg p = 1 )assume AS:
p is
irreducible
;
deg p = 1then
not
p is
constant
;
then
((len p) - 1) + 1
> 0 + 1
by XREAL_1:6;
then consider x being
Element of
R such that A:
x is_a_root_of p
by POLYNOM5:def 8, POLYNOM5:def 9;
consider q being
Polynomial of
R such that B:
p = (rpoly (1,x)) *' q
by A, HURWITZ:33;
reconsider y =
q,
z =
rpoly (1,
x) as
Element of
(Polynom-Ring R) by POLYNOM3:def 10;
p = z * y
by B, POLYNOM3:def 10;
then
z divides p
;
then C:
(
z is
Unit of
(Polynom-Ring R) or
z is_associated_to p )
by AS, RING_2:def 9;
not
z is
constant
by HURWITZ:27;
then consider e being
Element of
(Polynom-Ring R) such that D:
(
e is
unital &
z * e = p )
by C, GCD_1:18;
reconsider u =
e as
Element of the
carrier of
(Polynom-Ring R) ;
F:
deg u = 0
by D, T88;
(rpoly (1,x)) *' u = p
by D, POLYNOM3:def 10;
hence deg p =
(deg (rpoly (1,x))) + (deg u)
by D, HURWITZ:23
.=
1
by F, HURWITZ:27
;
verum end;
hence
( p is irreducible iff deg p = 1 )
by thirr; verum