Theorem Ideal.emultiplicity_eq_emultiplicity_span

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) …

Deleted Ideal.emultiplicity_eq_emultiplicity_span View on Github →

2026-04-17 15:37

Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean

chore(RingTheory/DedekindDomain/Ideal/*): move decls into namespaces (#38133) …

Added Ideal.emultiplicity_eq_emultiplicity_span View on Github →