Commit 2025-06-12 07:14 28fefce7
View on Github →feat(RingTheory/Polynomial/ContentIdeal): the content ideal of a polynomial. (#25333) We define the content ideal of a polynomial as
def contentIdeal (p : R[X]) := span p.coeffs.toSet
and prove some basic results in connection with the concept of content and primitivitiy. Zulip discussion here