From dad88d8c135ad4f25aacf5476e24953f47c61c37 Mon Sep 17 00:00:00 2001 From: tb65536 Date: Mon, 14 Dec 2020 13:16:18 +0000 Subject: [PATCH] feat(field_theory/splitting_field): add splits_X theorem (#5343) This is a handy result and isn't definitionally a special case of splits_X_sub_C --- src/field_theory/splitting_field.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/field_theory/splitting_field.lean b/src/field_theory/splitting_field.lean index b8435f2f41056..43c010845d6e0 100644 --- a/src/field_theory/splitting_field.lean +++ b/src/field_theory/splitting_field.lean @@ -101,6 +101,9 @@ splits_of_splits_of_dvd i one_ne_zero (splits_one _) $ is_unit_iff_dvd_one.1 hu theorem splits_X_sub_C {x : α} : (X - C x).splits i := splits_of_degree_eq_one _ $ degree_X_sub_C x +theorem splits_X : X.splits i := +splits_of_degree_eq_one _ $ degree_X + theorem splits_id_iff_splits {f : polynomial α} : (f.map i).splits (ring_hom.id β) ↔ f.splits i := by rw [splits_map_iff, ring_hom.id_comp]