English
If deg((p.map i)) ≤ 1 and f.Splits i, then (f.comp p).Splits i.
Русский
Если deg((p.map i)) ≤ 1 и f разбивается по i, то (f.comp p).Splits i.
LaTeX
$$hd : (p.map i).degree ≤ 1 → h : f.Splits i → (f.comp p).Splits i$$
Lean4
theorem comp_of_map_degree_le_one {f : K[X]} {p : K[X]} (hd : (p.map i).degree ≤ 1) (h : f.Splits i) :
(f.comp p).Splits i := by
by_cases hzero : map i (f.comp p) = 0
· exact Or.inl hzero
cases h with
| inl h0 => exact Or.inl <| map_comp i _ _ ▸ h0.symm ▸ zero_comp
| inr h =>
right
intro g irr dvd
rw [map_comp] at dvd hzero
cases lt_or_eq_of_le hd with
| inl hd =>
rw [eq_C_of_degree_le_zero (Nat.WithBot.lt_one_iff_le_zero.mp hd), comp_C] at dvd hzero
refine False.elim (irr.1 (isUnit_of_dvd_unit dvd ?_))
simpa using hzero
| inr
hd =>
let _ := invertibleOfNonzero (leadingCoeff_ne_zero.mpr (ne_zero_of_degree_gt (n := ⊥) (by rw [hd]; decide)))
rw [eq_X_add_C_of_degree_eq_one hd, dvd_comp_C_mul_X_add_C_iff _ _] at dvd
have := h (irr.map (algEquivCMulXAddC _ _).symm) dvd
rw [degree_eq_natDegree irr.ne_zero]
rwa [algEquivCMulXAddC_symm_apply, ← comp_eq_aeval, degree_eq_natDegree (fun h => WithBot.bot_ne_one (h ▸ this)),
natDegree_comp, natDegree_C_mul (invertibleInvOf.ne_zero), natDegree_X_sub_C, mul_one] at this
