English
For a polynomial p over a field K, the factorization of the ideal span of p matches the span of the factors of p.
Русский
Для многочлена p над полем K, факторизация идеала порожденного p соответствует линейному сочетанию порожденных его множителей.
LaTeX
$$factors (span {p}) = map (span {·}) (factors p)$$
Lean4
theorem factors_span_eq {p : K[X]} : factors (span { p }) = (factors p).map (fun q ↦ span { q }) :=
by
rcases eq_or_ne p 0 with rfl | hp; · simpa [Set.singleton_zero] using normalizedFactors_zero
have : ∀ q ∈ (factors p).map (fun q ↦ span { q }), Prime q := fun q hq ↦
by
obtain ⟨r, hr, rfl⟩ := Multiset.mem_map.mp hq
exact prime_span_singleton_iff.mpr <| prime_of_factor r hr
rw [← span_singleton_eq_span_singleton.mpr (factors_prod hp), ← multiset_prod_span_singleton,
factors_eq_normalizedFactors, normalizedFactors_prod_of_prime this]
