feat(FieldTheory): add results about minpoly

[mariainesdff]

---

[mathlib-bors[bot]]

:v: mariainesdff can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[github-actions[bot]]

PR summary

Import changes

No significant changes to the import graph

---

Declarations diff

+ aeval_algHom + algEquiv + algEquivOfAssociated + algEquivOfAssociated_apply_root + algEquivOfAssociated_toAlgHom + algEquivOfEq + algEquivOfEq_apply_root + algEquivOfEq_toAlgHom + algEquiv_apply + algHomOfDvd + algHomOfDvd_apply_root + coe_algEquivOfAssociated + coe_algEquivOfEq + coe_algHomOfDvd + eq_of_root + exists_algEquiv_of_root + exists_algEquiv_of_root'

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[mariainesdff]

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style