Commit 2024-06-10 12:50 1dd79a5d

View on Github →

feat(FieldTheory): add results about minpoly (#12450)

Estimated changes

Modified Mathlib/FieldTheory/Adjoin.lean

added theorem AdjoinRoot.algEquivOfAssociated_apply_root

added theorem AdjoinRoot.algEquivOfAssociated_toAlgHom

added theorem AdjoinRoot.algEquivOfEq_apply_root

added theorem AdjoinRoot.algEquivOfEq_toAlgHom

added theorem AdjoinRoot.algHomOfDvd_apply_root

added theorem AdjoinRoot.coe_algEquivOfAssociated

added theorem AdjoinRoot.coe_algEquivOfEq

added theorem AdjoinRoot.coe_algHomOfDvd

added theorem minpoly.algEquiv_apply

added theorem minpoly.eq_of_root

Modified Mathlib/FieldTheory/Minpoly/Basic.lean

added theorem minpoly.aeval_algHom

Modified Mathlib/FieldTheory/Normal.lean

added theorem minpoly.exists_algEquiv_of_root'

added theorem minpoly.exists_algEquiv_of_root

Modified scripts/style-exceptions.txt