Theorem traceForm_dualSubmodule_adjoin

Modification history

2023-12-26 13:18
Mathlib/RingTheory/DedekindDomain/Different.lean
feat: derivative of minpoly is in the different ideal. (#9283)
Added traceForm_dualSubmodule_adjoinView on Github →