Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-29 13:20 8faf8df0

View on Github →

feat(field_theory/splitting_field): splits predicate on polynomials

Estimated changes

Modified src/data/polynomial.lean

added theorem polynomial.degree_eq_degree_of_associated

added theorem polynomial.eq_X_add_C_of_degree_eq_one

Created src/field_theory/splitting_field.lean

added theorem polynomial.exists_multiset_of_splits

added theorem polynomial.exists_root_of_splits

added def polynomial.splits

added theorem polynomial.splits_C

added theorem polynomial.splits_comp_of_splits

added theorem polynomial.splits_iff_exists_multiset

added theorem polynomial.splits_map_iff

added theorem polynomial.splits_mul

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_splits_id

added theorem polynomial.splits_of_splits_mul

added theorem polynomial.splits_zero

Modified src/ring_theory/unique_factorization_domain.lean

added theorem unique_factorization_domain.exists_mem_factors_of_dvd