Commit 2025-06-03 18:34 117328da

View on Github →

feat(NumberTheory.KummerDedekind): add more results about the conductor of an algebraic integer (#25316) We complete the proof of:

theorem conductor_eq_top_iff_adjoin_eq_top {x : S} :
     conductor R x = ⊤ ↔ Algebra.adjoin R {x} = ⊤ :=

by adding LHS implies RHS. Also, we make public a function in the construction of the main result of this file that will be useful in #25038

Estimated changes