Theorem Submodule.IsPrincipal.contentIdeal_eq_span_content_of_isPrincipal

Modification history

2025-06-12 07:14
Mathlib/RingTheory/Polynomial/ContentIdeal.lean
feat(RingTheory/Polynomial/ContentIdeal): the content ideal of a polynomial. (#25333) …
Added Submodule.IsPrincipal.contentIdeal_eq_span_content_of_isPrincipalView on Github →