Commit 2022-06-21 14:57 2d70b946

golf(data/polynomial): factorization into linear factors when #roots=degree (#14862)

• Golf the proofs of prod_multiset_X_sub_C_of_monic_of_roots_card_eq and C_leading_coeff_mul_prod_multiset_X_sub_C and move them from splitting_field.lean to ring_division.lean; instead of using the former to deduce the latter as is currently done in mathlib, we prove the latter first and deduce the former easily. Remove the less general auxiliary, private _of_field versions.
• Move pairwise_coprime_X_sub from field_division.lean to ring_division.lean. Rename it to pairwise_coprime_X_sub_C to conform with existing convention. Golf its proof using the more general new lemma is_coprime_X_sub_C_of_is_unit_sub.
• Golf monic.irreducible_of_irreducible_map, but it's essentially the same proof.