Theorem KummerDedekind.multiplicity_factors_map_eq_multiplicity

Modification history

2024-10-16 04:43
Mathlib/NumberTheory/KummerDedekind.lean
refactor(RingTheory/Multiplicity): split to Nat-valued `multiplicity` and ENat-valued `emultiplicity` (#16881) …
Deleted KummerDedekind.multiplicity_factors_map_eq_multiplicityView on Github →
2024-07-31 19:18
Mathlib/NumberTheory/KummerDedekind.lean
Chore: Remove some uses of `open Classical` (#15371) …
Modified KummerDedekind.multiplicity_factors_map_eq_multiplicityView on Github →
2023-06-19 15:02
Mathlib/NumberTheory/KummerDedekind.lean
feat: port NumberTheory.KummerDedekind (#5249)
Added KummerDedekind.multiplicity_factors_map_eq_multiplicityView on Github →