Commit 2023-12-26 13:18 08636fb9

View on Github →

feat: derivative of minpoly is in the different ideal. (#9283)

Estimated changes

Modified Mathlib/NumberTheory/KummerDedekind.lean

added theorem mem_coeSubmodule_conductor

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

added theorem aeval_derivative_mem_differentIdeal

added theorem conductor_mul_differentIdeal

added theorem traceForm_dualSubmodule_adjoin