English
If Normal K L, then the polynomial map of c.minpoly under algebraMap K L equals the product over x in c.carrier.toFinset of (X − C x).
Русский
Если K ⊆ L нормально, то отображение минимального полинома через алгебраическое отображение равно произведению по x ∈ carrier(c) величин (X − C x).
LaTeX
$$$ c.minpoly.map(\\operatorname{algebraMap} K L) = \\prod_{x \\in c.carrier.toFinset} (X - C x) $$$
Lean4
theorem map_eq_prod [Normal K L] (c : ConjRootClass K L) [Fintype c.carrier] :
c.minpoly.map (algebraMap K L) = ∏ x ∈ c.carrier.toFinset, (X - C x) := by
classical
simp_rw [← rootSet_minpoly_eq_carrier, Finset.prod_eq_multiset_prod, rootSet_def, Finset.toFinset_coe,
Multiset.toFinset_val]
rw [Multiset.dedup_eq_self.mpr (nodup_roots c.separable_minpoly.map),
prod_multiset_X_sub_C_of_monic_of_roots_card_eq (c.monic_minpoly.map _)]
rw [← splits_iff_card_roots, splits_id_iff_splits]
exact c.splits_minpoly
