mathlib documentation

ring_theory.complex

Lemmas about algebra.trace and algebra.norm on #