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]]
Mathlib.RingTheory.Complex
Algebra.trace
and Algebra.norm
on ℂ
#