Commit 2021-08-27 14:36 dcd60e25

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.