Unique factorization of complex polynomials

Stream: Is there code for X?

[Yakov Pechersky]

Is there a neater way to do this? I feel like there is some missing API.

import field_theory.ratfunc
import data.complex.basic
import analysis.complex.polynomial

variables {R S K : Type*} [comm_ring R] [ring S] [field K]

namespace polynomial

lemma roots_eq_zero_iff [is_alg_closed K] {p : polynomial K} :
  p.roots = 0 ↔ p = polynomial.C (p.coeff 0) := sorry

lemma leading_coeff_div_by_X_sub_C (p : polynomial R) (hp : 0 < degree p) (a : R) :
  leading_coeff (p /ₘ (X - C a)) = leading_coeff p := sorry

lemma roots_div_X_sub_C [decidable_eq R] [is_domain R] (p : polynomial R) (r : R) :
  roots (p /ₘ (X - C r)) = (roots p).erase r := sorry

-- any polynomial (over the complexes) can be uniquely expressed as
-- P(X) = α(X − α₁)(X − α₂)...(X − αₙ)
-- where α, α₁, α₂, ..., αₙ are complex numbers
example (p : polynomial ℂ) : ∃ (α : ℂ) (f : multiset ℂ),
  p = α • (f.map (λ a, (polynomial.X : polynomial ℂ) - polynomial.C a)).prod :=
begin
  by_cases hp : p = 0,
  { refine ⟨0, 0, _⟩,
    simp [hp] },
  refine ⟨p.leading_coeff, p.roots, _⟩,
  rw smul_eq_C_mul,
  induction f : p.roots using multiset.induction_on with r rs IH generalizing p,
  { rw roots_eq_zero_iff at f,
    rw f,
    simp },
  { have hr : is_root p r,
    { simp [←mem_roots hp, f] },
    specialize IH (p /ₘ (X - C r)) _,
    { intro H,
      simpa [←mul_div_by_monic_eq_iff_is_root, H, ne.symm hp] using hr },
    have hd : 0 < degree p,
    { rw ←nat.with_bot.one_le_iff_zero_lt,
      refine le_trans _ (card_roots hp),
      rw [f, ←with_bot.coe_one, with_bot.coe_le_coe, multiset.card_cons],
      exact le_add_self },
    rw [multiset.map_cons, multiset.prod_cons, mul_left_comm, ←leading_coeff_div_by_X_sub_C _ hd r,
        ←IH, eq_comm, mul_div_by_monic_eq_iff_is_root.mpr hr],
    rw [roots_div_X_sub_C, f, multiset.erase_cons_head] }
end

[Yakov Pechersky]

Perhaps using unique_factorization_monoid.exists_prime_factors, but that is only up to associated.

[Yakov Pechersky]

The only sorry I don't have proven here is the roots_div_X_sub_C

[Riccardo Brasca]

docs#polynomial.C_leading_coeff_mul_prod_multiset_X_sub_C says more or less the same

[Riccardo Brasca]

Using docs#polynomial.splits_iff_card_roots

[Riccardo Brasca]

And of course docs#complex.is_alg_closed

[Yakov Pechersky]

Aha, you're going through C_leading_coeff_mul_prod_multiset_X_sub_C_of_field and prod_multiset_X_sub_C_of_monic_of_roots_card_eq

[Yakov Pechersky]

I must have been operating at too low an API level