theorem mmu: :: FIELD_10:11

for F being Field
for E being b₁ -finite FieldExtension of F
for a being Element of E holds deg (MinPoly (a,F)) divides deg (E,F)