Commit 2025-10-23 00:03 41772ea3
View on Github →feat(Algebra/Polynomial/Factors): Introduce predicate and basic API (#30212)
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