Theorem Ideal.spanSubmonoid_le_isPrincipalSubmonoid

Modification history

2026-10-18 08:25
Mathlib/RingTheory/Ideal/IsPrincipal.lean
feat(RingTheory/FractionalIdeal): add HasUniqueRoots instance (#40636) …
Added Ideal.spanSubmonoid_le_isPrincipalSubmonoidView on Github →