Lemmas about Algebra.trace and Algebra.norm on ℂ

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

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

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

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