mathlib documentation

ring_theory.complex

Lemmas about algebra.trace and algebra.norm on ℂ #

source
theorem algebra.left_mul_matrix_complex (z : ℂ) :
⇑(algebra.left_mul_matrix complex.basis_one_I) z = ⇑matrix.of ![![z.re, -z.im], ![z.im, z.re]]
source
theorem algebra.trace_complex_apply (z : ℂ) :
⇑(algebra.trace ℝ ℂ) z = 2 * z.re
source
theorem algebra.norm_complex_apply (z : ℂ) :
⇑(algebra.norm ℝ) z = ⇑complex.norm_sq z
source
theorem algebra.norm_complex_eq  :
algebra.norm ℝ = complex.norm_sq.to_monoid_hom