Theorem Ideal.span_singleton_mem_spanSubmonoid

Modification history

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