Multiplication by i on a complex seminormed space

Multiplication by i is a real continuous linear automorphism of any complex seminormed 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 any type with a complex multiplication action.
• 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} [MulAction ℂ X] (x : X) : I • -I • x = x

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

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

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

Equations

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

@[simp]

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

@[simp]

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