theorem multiiso: :: FIELD_15:63

for F being Field
for p being non zero Polynomial of F
for E1, E2 being FieldExtension of F
for i being Function of E1,E2 st i is F -fixing & i is isomorphism holds
for a being Element of E1 holds multiplicity (p,a) = multiplicity (p,(i . a))