mathlib

9015c511 - feat(ring_theory/complex): trace and norm of a complex number (#18658)