Commit 2025-06-17 13:09 d9d3b4ca

feat(RingTheory/Polynomial/ContentIdeal): more theorems (#25960) We prove more facts about contentIdeal. For instance we prove that (p * q).contentIdeal $\le$ p.contentIdeal * q.contentIdeal $\le$ (p * q).contentIdeal.radical which implies the following result, often called Gauss' Lemma

Polynomial.contentIdeal_mul_eq_top_of_contentIdeal_eq_top {p q : R[X]} (hp : p.contentIdeal = ⊤) 
(hq : q.contentIdeal = ⊤) : (p * q).contentIdeal = ⊤

Zulip discussion here