Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-15 06:43 a0ae2165

View on Github →

feat(field_theory/splitting_field): generalize splits for comm_ring K (#16405) The definition of splits has been slightly changed for this change. Hence 2 lemmas splits_iff and splits.def are added for the field K case. I guess it may be helpful if we are able to talk about something like splits i (p : ℤ[X])?

Estimated changes

Modified src/field_theory/abel_ruffini.lean

Modified src/field_theory/normal.lean

Modified src/field_theory/splitting_field.lean

added theorem polynomial.degree_eq_card_roots'

modified theorem polynomial.degree_eq_one_of_irreducible_of_splits

added theorem polynomial.exists_root_of_splits'

added theorem polynomial.map_root_of_splits'

added theorem polynomial.nat_degree_eq_card_roots'

added def polynomial.root_of_splits'

added theorem polynomial.root_of_splits'_eq_root_of_splits

added theorem polynomial.roots_ne_zero_of_splits'

added theorem polynomial.splits.def

modified theorem polynomial.splits_C

added theorem polynomial.splits_iff

modified theorem polynomial.splits_of_is_unit

added theorem polynomial.splits_of_map_degree_eq_one

added theorem polynomial.splits_of_map_eq_C

modified theorem polynomial.splits_of_splits_id

added theorem polynomial.splits_of_splits_mul'

modified theorem polynomial.splits_zero