Commit 2021-03-21 03:35 abfddbf8

feat(ring_theory): define left_mul_matrix and algebra.trace (#6653) This PR defines the algebra trace, and the bilinear trace form, for an algebra S over a ring R, for example a field extension L / K. Follow-up PRs will prove that algebra.trace K L x is the sum of the conjugate roots of x in L, that trace_form is nondegenerate and that trace K L x is integral over K. Then we'll use this to find an integral basis for field extensions, and then we can prove that the integral closure of a Dedekind domain is again a Dedekind domain.