Def conductor

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 View on Github →

2023-06-19 15:02

Mathlib/NumberTheory/KummerDedekind.lean

feat: port NumberTheory.KummerDedekind (#5249)

Added conductor View on Github →