Commit 2022-10-19 07:41 813725f8

View on Github →

feat(number_theory/kummer_dedekind): define conductor and add basic API plus theorem (#16833) In this PR we define the conductor ideal and prove some basic results about it. In a later PR (#16870), these will be used to prove the Dedekind-Kummer theorem in full generality.

Estimated changes

Modified src/number_theory/kummer_dedekind.lean

added theorem comap_map_eq_map_adjoin_of_coprime_conductor

added def conductor

added theorem conductor_eq_of_eq

added theorem conductor_subset_adjoin

added theorem mem_conductor_iff

added theorem prod_mem_ideal_map_of_mem_conductor

added theorem quot_adjoin_equiv_quot_map_apply_mk

Modified src/ring_theory/ideal/operations.lean

added theorem ring_hom.lift_injective_of_ker_le_ideal

Modified src/ring_theory/ideal/quotient.lean

added theorem ideal.quotient.lift_surjective_of_surjective