Theorem Ideal.span_singleton_dvd_span_singleton_iff_dvd

Modification history

2026-09-07 13:44
Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
feat(RingTheory/Ideal): generalize span_singleton_dvd_span_singleton_iff_dvd and emultiplicity_eq_emultiplicity_span (#40557) …
Modified Ideal.span_singleton_dvd_span_singleton_iff_dvdView on Github →
2026-04-17 15:37
Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
chore(RingTheory/DedekindDomain/Ideal/*): move decls into namespaces (#38133) …
Added Ideal.span_singleton_dvd_span_singleton_iff_dvdView on Github →