Lemmas about Algebra.trace and Algebra.norm on ℂ

theorem Algebra.leftMulMatrix_complex (z : ℂ) : ↑(Algebra.leftMulMatrix Complex.basisOneI) z = ↑Matrix.of ![![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