English
For a finite set s and a monic f ∈ s, the coefficient map under the splitting-field homomorphism sends (subProdXSubC f).coeff n to 0 for all n.
Русский
Для множества s и f ∈ s коэффициентная карта под гомоморфизмом в разложение поля отправляет коэффициент (subProdXSubC f).coeff n в 0 для всех n.
LaTeX
$$$toSplittingField\\; s((subProdXSubC f).coeff n) = 0$ for all n whenever f ∈ s$$
Lean4
theorem toSplittingField_coeff {s : Finset (Monics k)} {f} (h : f ∈ s) (n) :
toSplittingField s ((subProdXSubC f).coeff n) = 0 := by
classical
simp_rw [← AlgHom.coe_toRingHom, ← coeff_map, subProdXSubC, Polynomial.map_sub, Polynomial.map_prod,
Polynomial.map_sub, map_X, map_C, toSplittingField, AlgHom.coe_toRingHom, MvPolynomial.aeval_X, dif_pos h, ←
(finEquivRoots (Monics.splits_finsetProd h)).symm.prod_comp, Equiv.apply_symm_apply]
rw [Finset.prod_coe_sort (f := fun x : _ × ℕ ↦ X - C x.1), (Multiset.toEnumFinset _) |>.prod_eq_multiset_prod, ←
Function.comp_def (X - C ·) Prod.fst, ← Multiset.map_map, Multiset.map_toEnumFinset_fst, map_map,
AlgHom.comp_algebraMap]
conv in map _ _ => rw [eq_prod_roots_of_splits (Monics.splits_finsetProd h)]
rw [f.2, map_one, C_1, one_mul, sub_self, coeff_zero]
