Theorem conductor_eq_top_iff_adjoin_eq_top

Modification history

2025-09-03 11:07
Mathlib/NumberTheory/KummerDedekind.lean
chore(RingTheory/Conductor): move definition and results about the conductor ideal to a separate file (#29173) …
Modified conductor_eq_top_iff_adjoin_eq_topView on Github →
2025-06-03 18:34
Mathlib/NumberTheory/KummerDedekind.lean
feat(NumberTheory.KummerDedekind): add more results about the conductor of an algebraic integer (#25316) …
Added conductor_eq_top_iff_adjoin_eq_topView on Github →