feat(Algebra/Polynomial/Factors): Introduce predicate and basic API

[tb65536]

This PR introduces a predicate Polynomial.Factors that generalizes Polynomial.Splits beyond fields. This PR contains the definition of Polynomial.Factors along with most of API for Polynomial.Splits. The end goal is to either redefine Polynomial.Splits in terms of Polynomial.Factors or deprecate Polynomial.Splits entirely.

Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Generalizing.20.60Polynomial.2ESplits.60.20to.20rings

---

[github-actions]

PR summary 0607ff2a96

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Algebra.Polynomial.Factors (new file)	1246

---

Declarations diff

+ Factors
+ Factors.C
+ Factors.C_mul
+ Factors.C_mul_X_pow
+ Factors.X
+ Factors.X_add_C
+ Factors.X_pow
+ Factors.X_sub_C
+ Factors.eq_prod_roots
+ Factors.exists_eval_eq_zero
+ Factors.listProd
+ Factors.map
+ Factors.monomial
+ Factors.mul
+ Factors.multisetProd
+ Factors.natDegree_eq_card_roots
+ Factors.natDegree_le_one_of_irreducible
+ Factors.neg
+ Factors.of_degree_eq_one
+ Factors.of_degree_le_one
+ Factors.of_dvd
+ Factors.of_natDegree_eq_one
+ Factors.of_natDegree_le_one
+ Factors.one
+ Factors.pow
+ Factors.prod
+ Factors.roots_ne_zero
+ Factors.splits
+ Factors.zero
+ _root_.Polynomial.not_isUnit_X_add_C
+ factors_X_sub_C_mul_iff
+ factors_iff_exists_multiset
+ factors_iff_exists_multiset'
+ factors_iff_splits
+ factors_mul_iff
+ factors_neg_iff
+ factors_of_natDegree_eq_zero

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[kckennylau]

The end goal is to either redefine Polynomial.Splits in terms of Polynomial.Factors or deprecate Polynomial.Splits entirely.

(my personal opinion) I think this should be reflected in the docstring of both Polynomial.Splits and Polynomial.Factors.

[kckennylau]

I think all of these theorems could be tagged @[aesop] so it can do its magic automatically for a given goal like Factors (3 * (X - 1) * (X - 4))...

[tb65536]

I think all of these theorems could be tagged @[aesop] so it can do its magic automatically for a given goal like Factors (3 * (X - 1) * (X - 4))...

I've taken a stab at this, but let me know if anything looks off (I'm not so familiar with aesop).

[kckennylau]

Unfortunately I'm also not very familiar with aesop...

[erdOne]

Also it's a personal preference but maybe you would want to move some {f : R[X]} to variable?

[erdOne]

I just now realized that you are intentionally mimicking the Splits API. If any of the suggestions above will make your life harder when doing the refactor then feel free to ignore them. But perhaps leave the comment unresolved so that we can come back to this later.