Mathlib Changelog
v4
Changelog
About
Github
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