mathlib3

5948cde7 - feat(ring_theory): the field trace resp. norm is the sum resp. product of the conjugates (#7640)

feat(ring_theory): the field trace resp. norm is the sum resp. product of the conjugates (#7640) More precise statement of the main result: the field trace (resp. norm) of `x` in `K(x) / K`, mapped to a field `F` that contains all the conjugate roots over `K` of `x`, is equal to the sum (resp. product) of all of these conjugate roots. Co-authored-by: Johan Commelin <johan@commelin.net>