Lemmas about Algebra.trace and Algebra.norm on ℂ

theorem Algebra.leftMulMatrix_complex (z : ℂ) : (Algebra.leftMulMatrix Complex.basisOneI) z = !![z.re, -z.im; z.im, z.re]

theorem Algebra.trace_complex_apply (z : ℂ) : (Algebra.trace ℝ ℂ) z = 2 * z.re

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

theorem Algebra.norm_complex_eq : Algebra.norm ℝ = ↑Complex.normSq