Theorem mem_coeSubmodule_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 mem_coeSubmodule_conductorView on Github →
2023-12-26 13:18
Mathlib/NumberTheory/KummerDedekind.lean
feat: derivative of minpoly is in the different ideal. (#9283)
Added mem_coeSubmodule_conductorView on Github →