Commit 2022-09-16 22:29 1e225257

View on Github →

feat(number_theory): Dedekind-Kummer theorem (#15000) It's PR #15000! The Kummer-Dedekind theorem on the splitting of ideals in monogenic ring extensions. Zulip thread Co-Authored-By: Paul Lezeau paul.lezeau@gmail.com

Estimated changes

Modified src/data/multiset/basic.lean

added theorem multiset.attach_count_eq_count_coe

added theorem multiset.attach_map_coe

Created src/number_theory/kummer_dedekind.lean

added theorem kummer_dedekind.ideal.irreducible_map_of_irreducible_minpoly

added theorem kummer_dedekind.multiplicity_factors_map_eq_multiplicity

added theorem kummer_dedekind.normalized_factors_ideal_map_eq_normalized_factors_min_poly_mk_map

Modified src/ring_theory/ideal/operations.lean

added theorem ideal.map_eq_bot_iff_of_injective