let B be Ring; for A being non degenerated Ring
for a being Element of A st A is Subring of B holds
In (a,B) is_integral_over A
let A be non degenerated Ring; for a being Element of A st A is Subring of B holds
In (a,B) is_integral_over A
let a be Element of A; ( A is Subring of B implies In (a,B) is_integral_over A )
assume A0:
A is Subring of B
; In (a,B) is_integral_over A
set p = <%(- a),(1. A)%>;
<%(- a),(1. A)%> . ((len <%(- a),(1. A)%>) -' 1) =
<%(- a),(1. A)%> . (2 -' 1)
by POLYNOM5:40
.=
<%(- a),(1. A)%> . (2 - 1)
by XREAL_1:233
.=
<%(- a),(1. A)%> . 1
;
then A2:
LC <%(- a),(1. A)%> = 1. A
by POLYNOM5:38;
A3: eval (<%(- a),(1. A)%>,a) =
(- a) + a
by POLYNOM5:47
.=
a - a
.=
0. A
by RLVECT_1:15
;
Ext_eval (<%(- a),(1. A)%>,(In (a,B))) =
In ((eval (<%(- a),(1. A)%>,a)),B)
by A0, Th16
.=
0. B
by A0, Lm5, A3
;
hence
In (a,B) is_integral_over A
by A2; verum