Theorem KummerDedekind.multiplicity_factors_map_eq_multiplicity

Modification history

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 →