Theorem Ideal.Quotient.span_singleton_one

Modification history

2025-05-03 07:23
Mathlib/RingTheory/Ideal/Quotient/Operations.lean
feat(Algebra): finiteness of associated primes (#24242) …
Added Ideal.Quotient.span_singleton_oneView on Github →