Commit 2023-03-27 15:03 de17926c

View on Github →

feat: port Data.Polynomial.Splits (#3107)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Polynomial/Splits.lean

added theorem Polynomial.Splits.def

added def Polynomial.Splits

added theorem Polynomial.adjoin_rootSet_eq_range

added theorem Polynomial.aeval_root_derivative_of_splits

added theorem Polynomial.degree_eq_card_roots'

added theorem Polynomial.degree_eq_card_roots

added theorem Polynomial.degree_eq_one_of_irreducible_of_splits

added theorem Polynomial.eq_X_sub_C_of_splits_of_single_root

added theorem Polynomial.eq_prod_roots_of_monic_of_splits_id

added theorem Polynomial.eq_prod_roots_of_splits

added theorem Polynomial.eq_prod_roots_of_splits_id

added theorem Polynomial.exists_root_of_splits'

added theorem Polynomial.exists_root_of_splits

added theorem Polynomial.image_rootSet

added theorem Polynomial.map_rootOfSplits'

added theorem Polynomial.map_rootOfSplits

added theorem Polynomial.mem_lift_of_splits_of_roots_mem_range

added theorem Polynomial.natDegree_eq_card_roots'

added theorem Polynomial.natDegree_eq_card_roots

added theorem Polynomial.prod_roots_eq_coeff_zero_of_monic_of_split

added def Polynomial.rootOfSplits'

added theorem Polynomial.rootOfSplits'_eq_rootOfSplits

added def Polynomial.rootOfSplits

added theorem Polynomial.roots_map

added theorem Polynomial.roots_ne_zero_of_splits'

added theorem Polynomial.roots_ne_zero_of_splits

added theorem Polynomial.splits_C

added theorem Polynomial.splits_X

added theorem Polynomial.splits_X_pow

added theorem Polynomial.splits_X_sub_C

added theorem Polynomial.splits_comp_of_splits

added theorem Polynomial.splits_id_iff_splits

added theorem Polynomial.splits_iff

added theorem Polynomial.splits_iff_card_roots

added theorem Polynomial.splits_iff_exists_multiset

added theorem Polynomial.splits_map_iff

added theorem Polynomial.splits_mul

added theorem Polynomial.splits_mul_iff

added theorem Polynomial.splits_of_degree_eq_one

added theorem Polynomial.splits_of_degree_le_one

added theorem Polynomial.splits_of_exists_multiset

added theorem Polynomial.splits_of_isUnit

added theorem Polynomial.splits_of_map_degree_eq_one

added theorem Polynomial.splits_of_map_eq_C

added theorem Polynomial.splits_of_natDegree_eq_one

added theorem Polynomial.splits_of_natDegree_le_one

added theorem Polynomial.splits_of_splits_gcd_left

added theorem Polynomial.splits_of_splits_gcd_right

added theorem Polynomial.splits_of_splits_id

added theorem Polynomial.splits_of_splits_mul'

added theorem Polynomial.splits_of_splits_mul

added theorem Polynomial.splits_of_splits_of_dvd

added theorem Polynomial.splits_one

added theorem Polynomial.splits_pow

added theorem Polynomial.splits_prod

added theorem Polynomial.splits_prod_iff

added theorem Polynomial.splits_zero

added theorem Polynomial.sum_roots_eq_nextCoeff_of_monic_of_split