Commit 2024-11-06 13:19 5e231ef0

View on Github →

chore(RingTheory/DedekindDomain/Ideal): generalize count_associates_factors_eq (#18388) Generalize count_associates_factors_eq so that it assumes IsDedekindDomain R.

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

modified theorem count_associates_factors_eq

Modified Mathlib/RingTheory/LaurentSeries.lean