Complex number as a vector space over ℝ

This file contains the following instances:

• Any •-structure (SMul, MulAction, DistribMulAction, Module, Algebra) on ℝ imbues a corresponding structure on ℂ. This includes the statement that ℂ is an ℝ algebra.
• any complex vector space is a real vector space;
• any finite-dimensional complex vector space is a finite-dimensional real vector space;
• the space of ℝ-linear maps from a real vector space to a complex vector space is a complex vector space.

It also defines bundled versions of four standard maps (respectively, the real part, the imaginary part, the embedding of ℝ in ℂ, and the complex conjugate):

• Complex.reLm (ℝ-linear map);
• Complex.imLm (ℝ-linear map);
• Complex.ofRealAm (ℝ-algebra (homo)morphism);
• Complex.conjAe (ℝ-algebra equivalence).

It also provides a universal property of the complex numbers Complex.lift, which constructs a ℂ →ₐ[ℝ] A into any ℝ-algebra A given a square root of -1.

In addition, this file provides a decomposition into realPart and imaginaryPart for any element of a StarModule over ℂ.

Notation

• ℜ and ℑ for the realPart and imaginaryPart, respectively, in the locale ComplexStarModule.

@[instance 90]

instance Complex.instSMulCommClassOfReal {R : Type u_1} {S : Type u_2} [SMul R ℝ] [SMul S ℝ] [SMulCommClass R S ℝ] : SMulCommClass R S ℂ

@[instance 90]

instance Complex.instIsScalarTowerOfReal {R : Type u_1} {S : Type u_2} [SMul R S] [SMul R ℝ] [SMul S ℝ] [IsScalarTower R S ℝ] : IsScalarTower R S ℂ

@[instance 90]

instance Complex.instIsCentralScalarOfReal {R : Type u_1} [SMul R ℝ] [SMul Rᵐᵒᵖ ℝ] [IsCentralScalar R ℝ] : IsCentralScalar R ℂ

@[instance_reducible, instance 90]

instance Complex.mulAction {R : Type u_1} [Monoid R] [MulAction R ℝ] : MulAction R ℂ

Equations

• Complex.mulAction = { toSMul := Complex.SMul.instSMulRealComplex, mul_smul := ⋯, one_smul := ⋯ }

@[instance_reducible, instance 90]

instance Complex.distribSMul {R : Type u_1} [DistribSMul R ℝ] : DistribSMul R ℂ

Equations

• Complex.distribSMul = { toSMul := Complex.SMul.instSMulRealComplex, smul_zero := ⋯, smul_add := ⋯ }

@[instance_reducible, instance 90]

instance Complex.instDistribMulActionOfReal {R : Type u_1} [Semiring R] [DistribMulAction R ℝ] : DistribMulAction R ℂ

Equations

• Complex.instDistribMulActionOfReal = { toSMul := Complex.distribSMul.toSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

@[instance_reducible, instance 100]

instance Complex.instModule {R : Type u_1} [Semiring R] [Module R ℝ] : Module R ℂ

Equations

• Complex.instModule = { toDistribMulAction := Complex.instDistribMulActionOfReal, add_smul := ⋯, zero_smul := ⋯ }

@[instance_reducible, instance 95]

instance Complex.instAlgebraOfReal {R : Type u_1} [CommSemiring R] [Algebra R ℝ] : Algebra R ℂ

Equations

• Complex.instAlgebraOfReal = { toSMul := Complex.SMul.instSMulRealComplex, algebraMap := Complex.ofRealHom.comp (algebraMap R ℝ), commutes' := ⋯, smul_def' := ⋯ }

instance Complex.instStarModuleReal : StarModule ℝ ℂ

@[simp]

theorem Complex.coe_algebraMap : ⇑(algebraMap ℝ ℂ) = ofReal

@[simp]

theorem AlgHom.map_coe_real_complex {A : Type u_3} [Semiring A] [Algebra ℝ A] (f : ℂ →ₐ[ℝ] A) (x : ℝ) : f ↑x = (algebraMap ℝ A) x

We need this lemma since Complex.coe_algebraMap diverts the simp-normal form away from AlgHom.commutes.

theorem Complex.algHom_ext {A : Type u_3} [Semiring A] [Algebra ℝ A] ⦃f g : ℂ →ₐ[ℝ] A⦄ (h : f I = g I) : f = g

Two ℝ-algebra homomorphisms from ℂ are equal if they agree on Complex.I.

theorem Complex.algHom_ext_iff {A : Type u_3} [Semiring A] [Algebra ℝ A] {f g : ℂ →ₐ[ℝ] A} : f = g ↔ f I = g I

noncomputable def Complex.basisOneI : Module.Basis (Fin 2) ℝ ℂ

ℂ has a basis over ℝ given by 1 and I.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complex.coe_basisOneI_repr (z : ℂ) : ⇑(basisOneI.repr z) = ![z.re, z.im]

@[simp]

theorem Complex.coe_basisOneI : ⇑basisOneI = ![1, I]

@[instance_reducible, instance 900]

instance Module.complexToReal (E : Type u_1) [AddCommGroup E] [Module ℂ E] : Module ℝ E

Register as an instance (with low priority) the fact that a complex vector space is also a real vector space.

Equations

• Module.complexToReal E = Module.restrictScalars ℝ ℂ E

@[instance_reducible, instance 900]

instance Algebra.complexToReal {A : Type u_1} [Semiring A] [Algebra ℂ A] : Algebra ℝ A

Register as an instance (with low priority) the fact that a complex algebra is also a real algebra.

Equations

• Algebra.complexToReal = Algebra.restrictScalars ℝ ℂ A

@[simp]

theorem Complex.coe_smul {E : Type u_1} [AddCommGroup E] [Module ℂ E] (x : ℝ) (y : E) : ↑x • y = x • y

@[instance 900]

instance SMulCommClass.complexToReal {M : Type u_1} {E : Type u_2} [AddCommGroup E] [Module ℂ E] [SMul M E] [SMulCommClass ℂ M E] : SMulCommClass ℝ M E

The scalar action of ℝ on a ℂ-module E induced by Module.complexToReal commutes with another scalar action of M on E whenever the action of ℂ commutes with the action of M.

instance IsScalarTower.complexToReal {M : Type u_1} {E : Type u_2} [AddCommGroup M] [Module ℂ M] [AddCommGroup E] [Module ℂ E] [SMul M E] [IsScalarTower ℂ M E] : IsScalarTower ℝ M E

The scalar action of ℝ on a ℂ-module E induced by Module.complexToReal associates with another scalar action of M on E whenever the action of ℂ associates with the action of M.

@[instance 900]

instance StarModule.complexToReal {E : Type u_1} [AddCommGroup E] [Star E] [Module ℂ E] [StarModule ℂ E] : StarModule ℝ E

def Complex.reLm : ℂ →ₗ[ℝ] ℝ

Linear map version of the real part function, from ℂ to ℝ.

Equations

• Complex.reLm = { toFun := fun (x : ℂ) => x.re, map_add' := Complex.add_re, map_smul' := Complex.reLm._proof_1 }

@[simp]

theorem Complex.reLm_coe : ⇑reLm = re

def Complex.imLm : ℂ →ₗ[ℝ] ℝ

Linear map version of the imaginary part function, from ℂ to ℝ.

Equations

• Complex.imLm = { toFun := fun (x : ℂ) => x.im, map_add' := Complex.add_im, map_smul' := Complex.imLm._proof_1 }

@[simp]

theorem Complex.imLm_coe : ⇑imLm = im

def Complex.ofRealAm : ℝ →ₐ[ℝ] ℂ

ℝ-algebra morphism version of the canonical embedding of ℝ in ℂ.

Equations

• Complex.ofRealAm = Algebra.ofId ℝ ℂ

@[simp]

theorem Complex.ofRealAm_coe : ⇑ofRealAm = ofReal

def Complex.conjAe : ℂ ≃ₐ[ℝ] ℂ

ℝ-algebra isomorphism version of the complex conjugation function from ℂ to ℂ

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complex.conjAe_coe : ⇑conjAe = ⇑(starRingEnd ℂ)

@[simp]

theorem Complex.toMatrix_conjAe : (LinearMap.toMatrix basisOneI basisOneI) ↑↑conjAe = !![1, 0; 0, -1]

The matrix representation of conjAe.

theorem Complex.real_algHom_eq_id_or_conj (f : ℂ →ₐ[ℝ] ℂ) : f = AlgHom.id ℝ ℂ ∨ f = ↑conjAe

The identity and the complex conjugation are the only two ℝ-algebra homomorphisms of ℂ.

def Complex.equivRealProdLm : ℂ ≃ₗ[ℝ] ℝ × ℝ

The natural LinearEquiv from ℂ to ℝ × ℝ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complex.equivRealProdLm_apply (a✝ : ℂ) : equivRealProdLm a✝ = (a✝.re, a✝.im)

@[simp]

theorem Complex.equivRealProdLm_symm_apply_im (a✝ : ℝ × ℝ) : (equivRealProdLm.symm a✝).im = a✝.2

@[simp]

theorem Complex.equivRealProdLm_symm_apply_re (a✝ : ℝ × ℝ) : (equivRealProdLm.symm a✝).re = a✝.1

theorem Complex.equivRealProdLm_symm_apply (p : ℝ × ℝ) : equivRealProdLm.symm p = ↑p.1 + ↑p.2 * I

def Complex.liftAux {A : Type u_1} [Ring A] [Algebra ℝ A] (I' : A) (hf : I' * I' = -1) : ℂ →ₐ[ℝ] A

There is an AlgHom from ℂ to any ℝ-algebra with an element that squares to -1.

See Complex.lift for this as an equiv.

Equations

• Complex.liftAux I' hf = AlgHom.ofLinearMap (Algebra.linearMap ℝ A ∘ₗ Complex.reLm + LinearMap.toSpanSingleton ℝ A I' ∘ₗ Complex.imLm) ⋯ ⋯

@[simp]

theorem Complex.liftAux_apply {A : Type u_1} [Ring A] [Algebra ℝ A] (I' : A) (hI' : I' * I' = -1) (z : ℂ) : (liftAux I' hI') z = (algebraMap ℝ A) z.re + z.im • I'

theorem Complex.liftAux_apply_I {A : Type u_1} [Ring A] [Algebra ℝ A] (I' : A) (hI' : I' * I' = -1) : (liftAux I' hI') I = I'

@[simp]

theorem Complex.adjoin_I : ℝ[I] = ⊤

@[simp]

theorem Complex.range_liftAux {A : Type u_1} [Ring A] [Algebra ℝ A] (I' : A) (hI' : I' * I' = -1) : (liftAux I' hI').range = ℝ[I']

def Complex.lift {A : Type u_1} [Ring A] [Algebra ℝ A] : { I' : A // I' * I' = -1 } ≃ (ℂ →ₐ[ℝ] A)

A universal property of the complex numbers, providing a unique ℂ →ₐ[ℝ] A for every element of A which squares to -1.

This can be used to embed the complex numbers in the Quaternions.

This isomorphism is named to match the very similar Zsqrtd.lift.

Equations

• Complex.lift = { toFun := fun (I' : { I' : A // I' * I' = -1 }) => Complex.liftAux ↑I' ⋯, invFun := fun (F : ℂ →ₐ[ℝ] A) => ⟨F Complex.I, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Complex.lift_symm_apply_coe {A : Type u_1} [Ring A] [Algebra ℝ A] (F : ℂ →ₐ[ℝ] A) : ↑(lift.symm F) = F I

@[simp]

theorem Complex.lift_apply {A : Type u_1} [Ring A] [Algebra ℝ A] (I' : { I' : A // I' * I' = -1 }) : lift I' = liftAux ↑I' ⋯

@[simp]

theorem Complex.liftAux_I : liftAux I I_mul_I = AlgHom.id ℝ ℂ

@[simp]

theorem Complex.liftAux_neg_I : liftAux (-I) ⋯ = ↑conjAe

theorem Complex.I_mem_skewAdjoint : I ∈ skewAdjoint ℂ

@[simp]

theorem Complex.I_smul_mem_skewAdjoint_iff_isSelfAdjoint {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {a : A} : I • a ∈ skewAdjoint A ↔ IsSelfAdjoint a

@[simp]

theorem Complex.isSelfAdjoint_I_smul_iff_mem_skewAdjoint {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {a : A} : IsSelfAdjoint (I • a) ↔ a ∈ skewAdjoint A

def skewAdjoint.negISMul {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] : ↥(skewAdjoint A) →ₗ[ℝ] ↥(selfAdjoint A)

Create a selfAdjoint element from a skewAdjoint element by multiplying by the scalar -Complex.I.

Equations

• skewAdjoint.negISMul = { toFun := fun (a : ↥(skewAdjoint A)) => ⟨-Complex.I • ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem skewAdjoint.negISMul_apply_coe {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] (a : ↥(skewAdjoint A)) : ↑(negISMul a) = -Complex.I • ↑a

theorem skewAdjoint.I_smul_neg_I {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] (a : ↥(skewAdjoint A)) : Complex.I • ↑(negISMul a) = ↑a

noncomputable def realPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] : A →ₗ[ℝ] ↥(selfAdjoint A)

The real part ℜ a of an element a of a star module over ℂ, as a linear map. This is just selfAdjointPart ℝ, but we provide it as a separate definition in order to link it with lemmas concerning the imaginaryPart, which doesn't exist in star modules over other rings.

Equations

• realPart = selfAdjointPart ℝ

noncomputable def imaginaryPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] : A →ₗ[ℝ] ↥(selfAdjoint A)

The imaginary part ℑ a of an element a of a star module over ℂ, as a linear map into the self adjoint elements. In a general star module, we have a decomposition into the selfAdjoint and skewAdjoint parts, but in a star module over ℂ we have realPart_add_I_smul_imaginaryPart, which allows us to decompose into a linear combination of selfAdjoints.

Equations

• imaginaryPart = skewAdjoint.negISMul ∘ₗ skewAdjointPart ℝ

def ComplexStarModule.termℜ : Lean.ParserDescr

The real part ℜ a of an element a of a star module over ℂ, as a linear map. This is just selfAdjointPart ℝ, but we provide it as a separate definition in order to link it with lemmas concerning the imaginaryPart, which doesn't exist in star modules over other rings.

Equations

• ComplexStarModule.termℜ = Lean.ParserDescr.node `ComplexStarModule.termℜ 1024 (Lean.ParserDescr.symbol "ℜ")

def ComplexStarModule.termℑ : Lean.ParserDescr

The imaginary part ℑ a of an element a of a star module over ℂ, as a linear map into the self adjoint elements. In a general star module, we have a decomposition into the selfAdjoint and skewAdjoint parts, but in a star module over ℂ we have realPart_add_I_smul_imaginaryPart, which allows us to decompose into a linear combination of selfAdjoints.

Equations

• ComplexStarModule.termℑ = Lean.ParserDescr.node `ComplexStarModule.termℑ 1024 (Lean.ParserDescr.symbol "ℑ")

theorem realPart_apply_coe {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] (a : A) : ↑(realPart a) = 2⁻¹ • (a + star a)

theorem imaginaryPart_apply_coe {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] (a : A) : ↑(imaginaryPart a) = -Complex.I • 2⁻¹ • (a - star a)

theorem realPart_add_I_smul_imaginaryPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] (a : A) : ↑(realPart a) + Complex.I • ↑(imaginaryPart a) = a

The standard decomposition of ℜ a + Complex.I • ℑ a = a of an element of a star module over ℂ into a linear combination of self adjoint elements.

@[simp]

theorem realPart_I_smul {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] (a : A) : realPart (Complex.I • a) = -imaginaryPart a

@[simp]

theorem imaginaryPart_I_smul {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] (a : A) : imaginaryPart (Complex.I • a) = realPart a

theorem realPart_smul {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] (z : ℂ) (a : A) : realPart (z • a) = z.re • realPart a - z.im • imaginaryPart a

theorem imaginaryPart_smul {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] (z : ℂ) (a : A) : imaginaryPart (z • a) = z.re • imaginaryPart a + z.im • realPart a

theorem skewAdjointPart_eq_I_smul_imaginaryPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] (x : A) : ↑((skewAdjointPart ℝ) x) = Complex.I • ↑(imaginaryPart x)

theorem imaginaryPart_eq_neg_I_smul_skewAdjointPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] (x : A) : ↑(imaginaryPart x) = -Complex.I • ↑((skewAdjointPart ℝ) x)

theorem IsSelfAdjoint.coe_realPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {x : A} (hx : IsSelfAdjoint x) : ↑(realPart x) = x

theorem IsSelfAdjoint.imaginaryPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {x : A} (hx : IsSelfAdjoint x) : _root_.imaginaryPart x = 0

theorem realPart_comp_subtype_selfAdjoint {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] : realPart ∘ₗ (selfAdjoint.submodule ℝ A).subtype = LinearMap.id

theorem imaginaryPart_comp_subtype_selfAdjoint {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] : imaginaryPart ∘ₗ (selfAdjoint.submodule ℝ A).subtype = 0

@[simp]

theorem selfAdjoint.realPart_coe {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {x : ↥(selfAdjoint A)} : realPart ↑x = x

@[simp]

theorem selfAdjoint.imaginaryPart_coe {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {x : ↥(selfAdjoint A)} : imaginaryPart ↑x = 0

theorem imaginaryPart_realPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {x : A} : imaginaryPart ↑(realPart x) = 0

theorem imaginaryPart_imaginaryPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {x : A} : imaginaryPart ↑(imaginaryPart x) = 0

theorem realPart_idem {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {x : A} : realPart ↑(realPart x) = realPart x

theorem realPart_imaginaryPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {x : A} : realPart ↑(imaginaryPart x) = imaginaryPart x

theorem realPart_surjective {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] : Function.Surjective ⇑realPart

theorem imaginaryPart_surjective {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] : Function.Surjective ⇑imaginaryPart

theorem ComplexStarModule.ext {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {x y : A} (h₁ : realPart x = realPart y) (h₂ : imaginaryPart x = imaginaryPart y) : x = y

theorem ComplexStarModule.ext_iff {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {x y : A} : x = y ↔ realPart x = realPart y ∧ imaginaryPart x = imaginaryPart y

theorem map_realPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {B : Type u_2} {F : Type u_3} [AddCommGroup B] [Module ℂ B] [StarAddMonoid B] [StarModule ℂ B] [FunLike F A B] [StarHomClass F A B] [LinearMapClass F ℂ A B] (f : F) (x : A) : f ↑(realPart x) = ↑(realPart (f x))

theorem map_imaginaryPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {B : Type u_2} {F : Type u_3} [AddCommGroup B] [Module ℂ B] [StarAddMonoid B] [StarModule ℂ B] [FunLike F A B] [StarHomClass F A B] [LinearMapClass F ℂ A B] (f : F) (x : A) : f ↑(imaginaryPart x) = ↑(imaginaryPart (f x))

@[simp]

theorem ker_imaginaryPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] : imaginaryPart.ker = selfAdjoint.submodule ℝ A

@[simp]

theorem imaginaryPart_eq_zero_iff {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {x : A} : imaginaryPart x = 0 ↔ IsSelfAdjoint x

theorem span_selfAdjoint {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] : Submodule.span ℂ ↑(selfAdjoint A) = ⊤

def Complex.selfAdjointEquiv : ↥(selfAdjoint ℂ) ≃ₗ[ℝ] ℝ

The natural ℝ-linear equivalence between selfAdjoint ℂ and ℝ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complex.selfAdjointEquiv_symm_apply (x : ℝ) : selfAdjointEquiv.symm x = ⟨↑x, ⋯⟩

@[simp]

theorem Complex.selfAdjointEquiv_apply (z : ↥(selfAdjoint ℂ)) : selfAdjointEquiv z = (↑z).re

theorem Complex.coe_selfAdjointEquiv (z : ↥(selfAdjoint ℂ)) : ↑(selfAdjointEquiv z) = ↑z

@[simp]

theorem realPart_ofReal (r : ℝ) : ↑(realPart ↑r) = ↑r

@[simp]

theorem imaginaryPart_ofReal (r : ℝ) : imaginaryPart ↑r = 0

theorem Complex.coe_realPart (z : ℂ) : ↑(realPart z) = ↑z.re

theorem star_mul_self_add_self_mul_star {A : Type u_1} [NonUnitalNonAssocRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [StarModule ℂ A] (a : A) : star a * a + a * star a = 2 • (↑(realPart a) * ↑(realPart a) + ↑(imaginaryPart a) * ↑(imaginaryPart a))

theorem star_mul_self_sub_self_mul_star {A : Type u_1} [NonUnitalNonAssocRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [StarModule ℂ A] (a : A) : star a * a - a * star a = 2 • Complex.I • (↑(realPart a) * ↑(imaginaryPart a) - ↑(imaginaryPart a) * ↑(realPart a))

theorem isStarNormal_iff_commute_realPart_imaginaryPart {A : Type u_1} [NonUnitalNonAssocRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [StarModule ℂ A] {x : A} : IsStarNormal x ↔ Commute ↑(realPart x) ↑(imaginaryPart x)

An element in a non-unital star ℂ-algebra is normal if and only if its real and imaginary parts commute.

theorem Commute.realPart_imaginaryPart {A : Type u_1} [NonUnitalNonAssocRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [StarModule ℂ A] (x : A) [IsStarNormal x] : Commute ↑(realPart x) ↑(imaginaryPart x)

theorem star_mul_self_eq_realPart_sq_add_imaginaryPart_sq {A : Type u_1} [NonUnitalNonAssocRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [StarModule ℂ A] (x : A) [hx : IsStarNormal x] : star x * x = ↑(realPart x) * ↑(realPart x) + ↑(imaginaryPart x) * ↑(imaginaryPart x)

theorem nonneg_iff_realPart_imaginaryPart {A : Type u_1} [NonUnitalRing A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Module ℂ A] [StarModule ℂ A] {a : A} : 0 ≤ a ↔ 0 ≤ realPart a ∧ imaginaryPart a = 0

theorem nonpos_iff_realPart_imaginaryPart {A : Type u_1} [NonUnitalRing A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Module ℂ A] [StarModule ℂ A] {a : A} : a ≤ 0 ↔ realPart a ≤ 0 ∧ imaginaryPart a = 0

theorem realPart_nonneg_of_nonneg {A : Type u_1} [NonUnitalRing A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Module ℂ A] [StarModule ℂ A] {a : A} (ha : 0 ≤ a) : 0 ≤ realPart a

theorem realPart_nonpos_of_nonpos {A : Type u_1} [NonUnitalRing A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Module ℂ A] [StarModule ℂ A] {a : A} (ha : a ≤ 0) : realPart a ≤ 0

theorem le_iff_realPart_imaginaryPart {A : Type u_1} [NonUnitalRing A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Module ℂ A] [StarModule ℂ A] {a b : A} : a ≤ b ↔ realPart a ≤ realPart b ∧ imaginaryPart a = imaginaryPart b

theorem imaginaryPart_eq_of_le {A : Type u_1} [NonUnitalRing A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Module ℂ A] [StarModule ℂ A] {a b : A} (hab : a ≤ b) : imaginaryPart a = imaginaryPart b

theorem realPart_mono {A : Type u_1} [NonUnitalRing A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Module ℂ A] [StarModule ℂ A] {a b : A} (hab : a ≤ b) : realPart a ≤ realPart b

@[simp]

theorem realPart_one {A : Type u_1} [Ring A] [StarRing A] [Module ℂ A] [StarModule ℂ A] : realPart 1 = 1

theorem mem_unitary_iff_isStarNormal_and_realPart_sq_add_imaginaryPart_sq_eq_one {A : Type u_1} [Ring A] [StarRing A] [Module ℂ A] [SMulCommClass ℂ A A] [IsScalarTower ℂ A A] [StarModule ℂ A] {x : A} : x ∈ unitary A ↔ IsStarNormal x ∧ ↑(realPart x) ^ 2 + ↑(imaginaryPart x) ^ 2 = 1

instance instStarHomClassOfSelfAdjointDecomposeOfStarOrderedRingOfStarModuleOfOrderHomClassOfLinearMapClassComplex {F : Type u_2} {E : Type u_3} {A : Type u_4} [AddCommGroup E] [PartialOrder E] [StarAddMonoid E] [SelfAdjointDecompose E] [Module ℂ E] [StarModule ℂ E] [NonUnitalRing A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [Module ℂ A] [StarModule ℂ A] [FunLike F E A] [OrderHomClass F E A] [LinearMapClass F ℂ E A] : StarHomClass F E A