mathlib3 documentation

ring_theory.complex

Lemmas about algebra.trace and algebra.norm on #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.