English
If (p.map i).degree = 1, then f.Splits i ↔ (f.comp p).Splits i.
Русский
Если deg( p.map i ) = 1, то f.Splits i ⇔ (f.comp p).Splits i.
LaTeX
$$hd : (p.map i).degree = 1 → (f.Splits i) ↔ (f.comp p).Splits i$$
Lean4
theorem splits_iff_comp_splits_of_degree_eq_one {f : K[X]} {p : K[X]} (hd : (p.map i).degree = 1) :
f.Splits i ↔ (f.comp p).Splits i :=
by
rw [← splits_id_iff_splits, ← splits_id_iff_splits (f := f.comp p), map_comp]
refine ⟨fun h => Splits.comp_of_map_degree_le_one (le_of_eq (map_id (R := L) ▸ hd)) h, fun h => ?_⟩
let _ := invertibleOfNonzero (leadingCoeff_ne_zero.mpr (ne_zero_of_degree_gt (n := ⊥) (by rw [hd]; decide)))
have : (map i f) = ((map i f).comp (map i p)).comp ((C ⅟(map i p).leadingCoeff * (X - C ((map i p).coeff 0)))) :=
by
rw [comp_assoc]
nth_rw 1 [eq_X_add_C_of_degree_eq_one hd]
simp only [coeff_map, invOf_eq_inv, mul_sub, ← C_mul, add_comp, mul_comp, C_comp, X_comp, ← mul_assoc]
simp
refine this ▸ Splits.comp_of_map_degree_le_one ?_ h
simp [degree_C (inv_ne_zero (Invertible.ne_zero (a := (map i p).leadingCoeff)))]
