English
For a monic polynomial f over the field k, its image under the canonical map to the algebraic closure equals the product over its roots in the closure.
Русский
Для монической многочлена f над полем k его образ в замыкании равен произведению линейных множителей над корнями в замыкании.
LaTeX
$$$f.1.map(\text{algebraMap } k (\text{AlgebraicClosure}(k))) = \prod_i \; \text{map}(\text{Ideal.Quotient.mk}(\maxIdeal k))\big(X - C(\MvPolynomial.X⟨f,i⟩)\big).$$$
Lean4
theorem map_eq_prod {f : Monics k} :
f.1.map (algebraMap k (AlgebraicClosure k)) =
∏ i, map (Ideal.Quotient.mk <| maxIdeal k) (X - C (MvPolynomial.X ⟨f, i⟩)) :=
by
ext
dsimp [AlgebraicClosure]
rw [← Ideal.Quotient.mk_comp_algebraMap, ← map_map, ← Polynomial.map_prod, ← sub_eq_zero, ← coeff_sub, ←
Polynomial.map_sub, ← subProdXSubC, coeff_map, Ideal.Quotient.eq_zero_iff_mem]
refine le_maxIdeal _ (Ideal.subset_span ⟨⟨f, _⟩, rfl⟩)
