mathlib3

dcd60e25 - feat(ring_theory/trace): the trace form is nondegenerate (#8777)

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.