Refactor field theory using IsConjRoot

[jjdishere]

As suggested in the PR review of #17783, there is a task of refactoring theorem statements in field theory using IsConjRoot.

Currently the definition of IsConjRoot is later than most of the field theory files, and all the results are located in one file. It could be moved to a much earlier place (immediately following the definition of minpoly). And we can spread these results to the proper place where they are first proved among field theory files.