Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-26 11:48 f7fc89d5

View on Github →

feat(number_theory/kummer_dedekind): the return of the Dedekind-Kummer theorem. (#16870) In this PR, we finish the proof of the general case of the Dedekind-Kummer theorem as stated in Neukirch, completing the work done in #15000.

Estimated changes

Modified src/field_theory/minpoly/is_integrally_closed.lean

added theorem minpoly.prime_of_is_integrally_closed

Modified src/number_theory/kummer_dedekind.lean

added theorem conductor_eq_top_of_adjoin_eq_top

added theorem conductor_eq_top_of_power_basis

modified theorem kummer_dedekind.multiplicity_factors_map_eq_multiplicity

Modified src/ring_theory/adjoin_root.lean

added theorem adjoin_root.is_domain_of_prime

added theorem adjoin_root.no_zero_smul_divisors_of_prime_of_degree_ne_zero

added theorem adjoin_root.of.injective_of_degree_ne_zero

Modified src/ring_theory/is_adjoin_root.lean

added theorem adjoin_root.is_adjoin_root_map_eq_mk

added theorem adjoin_root.is_adjoin_root_monic_map_eq_mk

added theorem adjoin_root.is_adjoin_root_monic_root_eq_root

added theorem adjoin_root.is_adjoin_root_root_eq_root

added theorem algebra.adjoin.power_basis'_minpoly_gen