Theorem IsIdempotentElem.ker_toSpanSingleton_one_sub_eq_span

Modification history

2024-11-25 16:30
Mathlib/RingTheory/Ideal/Span.lean
feat: ring with discrete PrimeSpectrum (#18891) …
Added IsIdempotentElem.ker_toSpanSingleton_one_sub_eq_spanView on Github →