Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(ring_theory/trace): the trace form is nondegenerate (#8777)
This PR shows the determinant of the trace form is nonzero over a finite separable field extension. This is an important ingredient in showing the integral closure of a Dedekind domain in a finite separable extension is again a Dedekind domain, i.e. that rings of integers are Dedekind domains. We extend the results of #8762 to write the trace form as a Vandermonde matrix to get a nice expression for the determinant, then use separability to show this value is nonzero.
- Loading branch information
1 parent
7f25698
commit dcd60e2
Showing
2 changed files
with
65 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters