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