Theorem Ideal.mem_span_range_self

Modification history

2025-10-06 17:04
Mathlib/RingTheory/Ideal/Span.lean
feat(RingTheory/Noetherian): add `IsNoetherianRing.of_prime` (#28451) …
Added Ideal.mem_span_range_selfView on Github →