Commit 2025-11-20 19:42 50f57fed

View on Github →

feat(Algebra/Polynomial/Splits): remove the RingHom argument of Splits (#31631)

Estimated changes

modified theorem Polynomial.Splits.def
modified theorem Polynomial.image_rootSet
modified theorem Polynomial.map_rootOfSplits
modified theorem Polynomial.roots_map
modified theorem Polynomial.splits_C
modified theorem Polynomial.splits_X
modified theorem Polynomial.splits_X_pow
modified theorem Polynomial.splits_X_sub_C
modified theorem Polynomial.splits_mul
modified theorem Polynomial.splits_of_algHom
modified theorem Polynomial.splits_of_comp
modified theorem Polynomial.splits_of_isUnit
modified theorem Polynomial.splits_one
modified theorem Polynomial.splits_pow
modified theorem Polynomial.splits_zero
modified theorem gal_isSolvable_tower
modified theorem Splits.algebraicClosure
modified theorem IsGalois.splits
modified theorem IsAlgClosed.splits
modified theorem Normal.out
modified theorem Normal.splits
modified theorem normal_iff
modified theorem Polynomial.Gal.smul_def
modified theorem minpoly_neg_splits
modified theorem Algebra.norm_eq_prod_roots