Multiplication by i on a complex normed space

Multiplication by i is a real continuous linear automorphism of any complex normed space, with inverse multiplication by -i. It is the conjugating operator by which complex linearity of a real-linear map is tested.

Main definitions and results

• Complex.I_smul_neg_I_smul and Complex.neg_I_smul_I_smul: multiplication by i and by -i are mutually inverse on a complex module.
• Complex.smulIEquiv: multiplication by i as a real continuous linear equivalence, with smulIEquiv_apply and smulIEquiv_symm_apply.

theorem Complex.I_smul_neg_I_smul {X : Type u_1} [AddCommGroup X] [Module ℂ X] (x : X) : I • -I • x = x

theorem Complex.neg_I_smul_I_smul {X : Type u_1} [AddCommGroup X] [Module ℂ X] (x : X) : -I • I • x = x

noncomputable def Complex.smulIEquiv (X : Type u_1) [NormedAddCommGroup X] [NormedSpace ℂ X] : X ≃L[ℝ] X

Multiplication by i as a real continuous linear equivalence of a complex normed space.

Equations

• Complex.smulIEquiv X = ContinuousLinearEquiv.smulLeft (Units.mk0 Complex.I Complex.I_ne_zero)

@[simp]

theorem Complex.smulIEquiv_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (x : X) : (smulIEquiv X) x = I • x

@[simp]

theorem Complex.smulIEquiv_symm_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (x : X) : (smulIEquiv X).symm x = -I • x