Commit 2023-06-19 15:02 a7b1b603

View on Github →

feat: port NumberTheory.KummerDedekind (#5249)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/KummerDedekind.lean

added theorem KummerDedekind.Ideal.irreducible_map_of_irreducible_minpoly

added theorem KummerDedekind.multiplicity_factors_map_eq_multiplicity

added theorem KummerDedekind.normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map

added theorem comap_map_eq_map_adjoin_of_coprime_conductor

added def conductor

added theorem conductor_eq_of_eq

added theorem conductor_eq_top_of_adjoin_eq_top

added theorem conductor_eq_top_of_powerBasis

added theorem conductor_subset_adjoin

added theorem mem_conductor_iff

added theorem prod_mem_ideal_map_of_mem_conductor

added theorem quotAdjoinEquivQuotMap_apply_mk