Theorem Ideal.mem_spanSubmonoid_iff

Modification history

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