Theorem Ideal.spanSubmonoid_top

Modification history

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