Commit 2025-09-03 11:07 906d09b3

View on Github →

chore(RingTheory/Conductor): move definition and results about the conductor ideal to a separate file (#29173) This PR moves the definition and API for the conductor ideal to a separate file (the Kummer-Dedekind theorem isn't the only place this arises in!) The list of authors of the file was reconstituted from the git history.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/NumberTheory/KummerDedekind.lean

deleted theorem adjoin_eq_top_of_conductor_eq_top

deleted theorem comap_map_eq_map_adjoin_of_coprime_conductor

deleted def conductor

deleted theorem conductor_eq_of_eq

deleted theorem conductor_eq_top_iff_adjoin_eq_top

deleted theorem conductor_eq_top_of_adjoin_eq_top

deleted theorem conductor_eq_top_of_powerBasis

deleted theorem conductor_subset_adjoin

deleted theorem mem_coeSubmodule_conductor

deleted theorem mem_conductor_iff

deleted theorem prod_mem_ideal_map_of_mem_conductor

deleted theorem quotAdjoinEquivQuotMap_apply_mk

Created Mathlib/RingTheory/Conductor.lean

added theorem adjoin_eq_top_of_conductor_eq_top

added theorem comap_map_eq_map_adjoin_of_coprime_conductor

added def conductor

added theorem conductor_eq_of_eq

added theorem conductor_eq_top_iff_adjoin_eq_top

added theorem conductor_eq_top_of_adjoin_eq_top

added theorem conductor_eq_top_of_powerBasis

added theorem conductor_subset_adjoin

added theorem mem_coeSubmodule_conductor

added theorem mem_conductor_iff

added theorem prod_mem_ideal_map_of_mem_conductor

added theorem quotAdjoinEquivQuotMap_apply_mk

Modified Mathlib/RingTheory/DedekindDomain/Different.lean