Commit 2021-06-12 02:38 5948cde7

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.