Def Ideal.spanSubmonoid

Modification history

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