theorem mp: :: FIELD_10:30

MinPoly (2-Root(2),F_Rat) = X^2-2