mathlib

abfddbf8 - feat(ring_theory): define `left_mul_matrix` and `algebra.trace` (#6653)

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. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>