Theorem KummerDedekind.Ideal.irreducible_map_of_irreducible_minpoly

Modification history

2023-06-19 15:02
Mathlib/NumberTheory/KummerDedekind.lean
feat: port NumberTheory.KummerDedekind (#5249)
Added KummerDedekind.Ideal.irreducible_map_of_irreducible_minpolyView on Github →