Commit 2023-12-11 20:22 556f6483

View on Github →

chore: cleanups following #8609 and #8714 (#8962)

  • generalize image_rootSet, adjoin_rootSet_eq_range and splits_comp_of_splits in Data/Polynomial/Splits and use the last one to golf splits_of_algHom, splits_of_isScalarTower (introduced in # 8609).
  • add three new lemmas mem_range_x_of_minpoly_splits to simplify the construction of IntermediateField.algHomEquivAlgHomOfIsAlgClosed and Algebra.IsAlgebraic.algHomEquivAlgHomOfIsAlgClosed, remove the IsAlgClosed condition and rename. They could be moved to an earlier file but I refrain from doing that. (#find_home says it's already in the right place)
  • golf primitive_element_iff_algHom_eq_of_eval from # 8609, using a new lemma IsIntegral.minpoly_splits_tower_top for the last step.
  • make integralClosure_algEquiv_restrict (from # 8714) computable and rename to AlgEquiv.mapIntegralClosure to follow camelCase naming convention and enable dot notation.

Estimated changes

modified theorem Polynomial.image_rootSet
modified theorem Polynomial.splits_of_algHom