Documentation

Mathlib.RingTheory.Complex

Lemmas about Algebra.trace and Algebra.norm on #

theorem Algebra.norm_complex_apply (z : ) :
(Algebra.norm ) z = Complex.normSq z