Module

📁 Source: Mathlib/LinearAlgebra/Complex/Module.lean

Statistics

Metric	Count
Definitions complexToReal, basisOneI, conjAe, distribSMul, equivRealProdLm, imLm, instAlgebraOfReal, instDistribMulActionOfReal, instModule, liftAux, mulAction, ofRealAm, reLm, selfAdjointEquiv, termℑ, termℜ, complexToReal, imaginaryPart, realPart, negISMul	20
Theorems map_coe_real_complex, adjoin_I, algHom_ext, algHom_ext_iff, coe_algebraMap, coe_basisOneI, coe_basisOneI_repr, coe_realPart, coe_selfAdjointEquiv, coe_smul, conjAe_coe, equivRealProdLm_apply, equivRealProdLm_symm_apply, equivRealProdLm_symm_apply_im, equivRealProdLm_symm_apply_re, imLm_coe, instIsCentralScalarOfReal, instIsScalarTowerOfReal, instSMulCommClassOfReal, instStarModuleReal, liftAux_I, liftAux_apply, liftAux_apply_I, liftAux_neg_I, lift_apply, lift_symm_apply_coe, ofRealAm_coe, range_liftAux, reLm_coe, real_algHom_eq_id_or_conj, selfAdjointEquiv_apply, selfAdjointEquiv_symm_apply, toMatrix_conjAe, complexToReal, coe_realPart, imaginaryPart, complexToReal, complexToReal, imaginaryPart_I_smul, imaginaryPart_apply_coe, imaginaryPart_comp_subtype_selfAdjoint, imaginaryPart_eq_neg_I_smul_skewAdjointPart, imaginaryPart_imaginaryPart, imaginaryPart_ofReal, imaginaryPart_realPart, imaginaryPart_smul, imaginaryPart_surjective, realPart_I_smul, realPart_add_I_smul_imaginaryPart, realPart_apply_coe, realPart_comp_subtype_selfAdjoint, realPart_idem, realPart_imaginaryPart, realPart_ofReal, realPart_smul, realPart_surjective, imaginaryPart_coe, realPart_coe, I_smul_neg_I, negISMul_apply_coe, skewAdjointPart_eq_I_smul_imaginaryPart, span_selfAdjoint, star_mul_self_add_self_mul_star	63
Total	83

AlgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_coe_real_complex 📖	mathematical	—	DFunLike.coe AlgHom Real Complex Real.instCommSemiring Complex.instSemiring Complex.instAlgebraOfReal Algebra.id funLike Complex.ofReal RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	commutes

Algebra

Definitions

Name	Category	Theorems
complexToReal 📖	CompOp	37 math math: Complex.ofRealCLM_coe, CliffordAlgebraComplex.ofComplex_conj, Complex.real_algHom_eq_id_or_conj, cfc_complex_eq_real, CliffordAlgebraComplex.ofComplex_toComplex, CliffordAlgebraComplex.toComplex_comp_ofComplex, Complex.liftAux_apply, IsSelfAdjoint.coe_mem_spectrum_complex, Complex.lift_apply, CliffordAlgebraComplex.ofComplex_I, Complex.liftAux_neg_I, Complex.det_conjAe, Complex.liftAux_I, Complex.range_liftAux, Complex.liftAux_apply_I, cfcHom_real_eq_restrict, IsSelfAdjoint.spectrumRestricts, norm_complex_eq, Complex.conjAe_coe, SpectrumRestricts.real_iff, CliffordAlgebraComplex.equiv_symm_apply, CliffordAlgebraComplex.toComplex_ι, Complex.linearEquiv_det_conjAe, norm_complex_apply, CliffordAlgebraComplex.equiv_apply, Complex.lift_symm_apply_coe, trace_complex_apply, IsSelfAdjoint.instContinuousFunctionalCalculus, Complex.toMatrix_conjAe, CliffordAlgebraComplex.toComplex_involute, CliffordAlgebraComplex.toComplex_ofComplex, Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv, cfc_real_eq_complex, Complex.adjoin_I, CliffordAlgebraComplex.ofComplex_comp_toComplex, Complex.ofRealAm_coe, Complex.conjCLE_coe

Complex

Definitions

Name	Category	Theorems
basisOneI 📖	CompOp	6 math math: toMatrix_rotation, toBasis_orthonormalBasisOneI, coe_basisOneI_repr, Algebra.leftMulMatrix_complex, toMatrix_conjAe, coe_basisOneI
conjAe 📖	CompOp	8 math math: real_algHom_eq_id_or_conj, liftAux_neg_I, det_conjAe, conjAe_coe, linearEquiv_det_conjAe, toMatrix_conjAe, Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv, conjCLE_coe
distribSMul 📖	CompOp	—
equivRealProdLm 📖	CompOp	4 math math: equivRealProdLm_apply, equivRealProdLm_symm_apply, equivRealProdLm_symm_apply_im, equivRealProdLm_symm_apply_re
imLm 📖	CompOp	3 math math: MeasureTheory.ComplexMeasure.im_apply, imCLM_coe, imLm_coe
instAlgebraOfReal 📖	CompOp	8 math math: toMatrix_rotation, algHom_ext_iff, coe_basisOneI_repr, Algebra.leftMulMatrix_complex, coe_algebraMap, AlgHom.map_coe_real_complex, toMatrix_conjAe, coe_basisOneI
instDistribMulActionOfReal 📖	CompOp	—
instModule 📖	CompOp	2 math math: MeasureTheory.ComplexMeasure.equivSignedMeasureₗ_symm_apply, MeasureTheory.ComplexMeasure.equivSignedMeasureₗ_apply
liftAux 📖	CompOp	6 math math: liftAux_apply, lift_apply, liftAux_neg_I, liftAux_I, range_liftAux, liftAux_apply_I
mulAction 📖	CompOp	—
ofRealAm 📖	CompOp	2 math math: ofRealCLM_coe, ofRealAm_coe
reLm 📖	CompOp	3 math math: reLm_coe, reCLM_coe, MeasureTheory.ComplexMeasure.re_apply
selfAdjointEquiv 📖	CompOp	3 math math: selfAdjointEquiv_apply, coe_selfAdjointEquiv, selfAdjointEquiv_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_I 📖	mathematical	—	Algebra.adjoin Real Complex Real.instCommSemiring instSemiring Algebra.complexToReal Algebra.id instCommSemiring Set Set.instSingletonSet I Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	top_unique re_add_im smul_eq_mul coe_algebraMap AddMemClass.add_mem AddSubmonoidClass.toAddMemClass SubsemiringClass.toAddSubmonoidClass Subalgebra.instSubsemiringClass algebraMap_mem AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass Subalgebra.instSMulMemClass Subalgebra.smul_mem Algebra.subset_adjoin
algHom_ext 📖	—	DFunLike.coe AlgHom Real Complex Real.instCommSemiring instSemiring instAlgebraOfReal Algebra.id AlgHom.funLike I	—	—	AlgHom.ext mk_eq_add_mul_I map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass AlgHom.map_coe_real_complex map_mul NonUnitalAlgSemiHomClass.toMulHomClass
algHom_ext_iff 📖	mathematical	—	DFunLike.coe AlgHom Real Complex Real.instCommSemiring instSemiring instAlgebraOfReal Algebra.id AlgHom.funLike I	—	algHom_ext
coe_algebraMap 📖	mathematical	—	DFunLike.coe RingHom Real Complex Semiring.toNonAssocSemiring CommSemiring.toSemiring Real.instCommSemiring instSemiring RingHom.instFunLike algebraMap instAlgebraOfReal Algebra.id ofReal	—	—
coe_basisOneI 📖	mathematical	—	DFunLike.coe Module.Basis Real Complex Real.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing Algebra.toModule Real.instCommSemiring instSemiring instAlgebraOfReal Algebra.id Module.Basis.instFunLike basisOneI Matrix.vecCons instOne I Matrix.vecEmpty	—	RingHomInvPair.ids Module.Basis.apply_eq_iff Finsupp.ext Fintype.complete Finsupp.single_eq_same Matrix.cons_val_fin_one Finsupp.single_eq_of_ne zero_add Nat.instCharZero Nat.instAtLeastTwoHAddOfNat
coe_basisOneI_repr 📖	mathematical	—	DFunLike.coe Finsupp Real MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Real.semiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids Complex NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing Finsupp.instAddCommMonoid Algebra.toModule Real.instCommSemiring instSemiring instAlgebraOfReal Algebra.id Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr basisOneI Matrix.vecCons re im Matrix.vecEmpty	—	RingHomInvPair.ids
coe_realPart 📖	mathematical	—	Complex AddSubgroup AddCommGroup.toAddGroup addCommGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing instStarRing DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal Semiring.toModule instSemiring selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid StarMul.toStarModule CommRing.toCommMonoid StarRing.toStarMul LinearMap.instFunLike realPart ofReal re	—	instTrivialStarReal StarModule.complexToReal StarMul.toStarModule re_add_im map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass AddSubmonoid.coe_add mul_comm smul_eq_mul realPart_I_smul realPart_ofReal imaginaryPart_ofReal neg_zero add_zero
coe_selfAdjointEquiv 📖	mathematical	—	ofReal DFunLike.coe LinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex AddSubgroup AddGroupWithOne.toAddGroup addGroupWithOne SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing instStarRing NonUnitalNonAssocSemiring.toAddCommMonoid selfAdjoint.instCommRingSubtypeMemAddSubgroup Real.instAddCommMonoid selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid Real.commRing instStarRingReal instTrivialStarReal addCommGroup Module.complexToReal Semiring.toModule instSemiring instStarModuleReal EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv selfAdjointEquiv	—	RingHomInvPair.ids instTrivialStarReal instStarModuleReal LinearEquiv.left_inv
coe_smul 📖	mathematical	—	Complex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid ofReal Real Real.instMonoid Real.semiring Module.complexToReal	—	—
conjAe_coe 📖	mathematical	—	DFunLike.coe AlgEquiv Real Complex Real.instCommSemiring instSemiring Algebra.complexToReal Algebra.id instCommSemiring AlgEquiv.instFunLike conjAe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike starRingEnd instStarRing	—	—
equivRealProdLm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing Prod.instAddCommMonoid Real.instAddCommMonoid Module.complexToReal addCommGroup Semiring.toModule instSemiring Prod.instModule EquivLike.toFunLike LinearEquiv.instEquivLike equivRealProdLm re im	—	RingHomInvPair.ids
equivRealProdLm_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex Prod.instAddCommMonoid Real.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing Prod.instModule Semiring.toModule Module.complexToReal addCommGroup instSemiring EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm equivRealProdLm instAdd ofReal instMul I	—	equivRealProd_symm_apply
equivRealProdLm_symm_apply_im 📖	mathematical	—	im DFunLike.coe LinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex Prod.instAddCommMonoid Real.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing Prod.instModule Semiring.toModule Module.complexToReal addCommGroup instSemiring EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm equivRealProdLm	—	RingHomInvPair.ids
equivRealProdLm_symm_apply_re 📖	mathematical	—	re DFunLike.coe LinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex Prod.instAddCommMonoid Real.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing Prod.instModule Semiring.toModule Module.complexToReal addCommGroup instSemiring EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm equivRealProdLm	—	RingHomInvPair.ids
imLm_coe 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing Real.instAddCommMonoid Module.complexToReal addCommGroup Semiring.toModule instSemiring LinearMap.instFunLike imLm im	—	—
instIsCentralScalarOfReal 📖	mathematical	—	IsCentralScalar Complex SMul.instSMulRealComplex MulOpposite	—	ext smul_re IsCentralScalar.op_smul_eq_smul smul_im
instIsScalarTowerOfReal 📖	mathematical	—	IsScalarTower Complex SMul.instSMulRealComplex	—	ext smul_re smul_assoc smul_im
instSMulCommClassOfReal 📖	mathematical	—	SMulCommClass Complex SMul.instSMulRealComplex	—	ext smul_re SMulCommClass.smul_comm smul_im
instStarModuleReal 📖	mathematical	—	StarModule Real Complex InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing StarRing.toStarAddMonoid instStarRingReal commRing instStarRing SMul.instSMulRealComplex Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id	—	map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass conj_ofReal TrivialStar.star_trivial instTrivialStarReal
liftAux_I 📖	mathematical	—	liftAux Complex instRing Algebra.complexToReal Ring.toSemiring Algebra.id instCommSemiring I I_mul_I AlgHom.id Real Real.instCommSemiring instSemiring	—	algHom_ext I_mul_I liftAux_apply_I
liftAux_apply 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	DFunLike.coe AlgHom Real Complex Real.instCommSemiring instSemiring Ring.toSemiring Algebra.complexToReal Algebra.id instCommSemiring AlgHom.funLike liftAux Distrib.toAdd RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap re Algebra.toSMul im	—	—
liftAux_apply_I 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	DFunLike.coe AlgHom Real Complex Real.instCommSemiring instSemiring Ring.toSemiring Algebra.complexToReal Algebra.id instCommSemiring AlgHom.funLike liftAux I	—	map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass one_smul zero_add
liftAux_neg_I 📖	mathematical	—	liftAux Complex CommRing.toRing commRing Algebra.complexToReal Ring.toSemiring Algebra.id instCommSemiring instNeg I Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing InvolutiveNeg.toNeg HasDistribNeg.toInvolutiveNeg NonUnitalNonAssocRing.toHasDistribNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne neg_mul_neg I_mul_I AlgHomClass.toAlgHom Real Real.instCommSemiring instSemiring AlgEquiv AlgEquiv.instFunLike AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass conjAe	—	algHom_ext neg_mul_neg I_mul_I AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass liftAux_apply_I conj_I
lift_apply 📖	mathematical	—	DFunLike.coe Equiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne AlgHom Real Complex Real.instCommSemiring instSemiring Ring.toSemiring Algebra.complexToReal Algebra.id instCommSemiring EquivLike.toFunLike Equiv.instEquivLike lift liftAux	—	—
lift_symm_apply_coe 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DFunLike.coe Equiv AlgHom Real Complex Real.instCommSemiring instSemiring Ring.toSemiring Algebra.complexToReal Algebra.id instCommSemiring EquivLike.toFunLike Equiv.instEquivLike Equiv.symm lift AlgHom.funLike I	—	—
ofRealAm_coe 📖	mathematical	—	DFunLike.coe AlgHom Real Complex Real.instCommSemiring Real.semiring instSemiring Algebra.id Algebra.complexToReal instCommSemiring AlgHom.funLike ofRealAm ofReal	—	—
range_liftAux 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	AlgHom.range Real Complex Real.instCommSemiring instSemiring Algebra.complexToReal Algebra.id instCommSemiring Ring.toSemiring liftAux Algebra.adjoin Set Set.instSingletonSet	—	AlgHom.map_adjoin Set.image_singleton liftAux_apply_I
reLm_coe 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing Real.instAddCommMonoid Module.complexToReal addCommGroup Semiring.toModule instSemiring LinearMap.instFunLike reLm re	—	—
real_algHom_eq_id_or_conj 📖	mathematical	—	AlgHom.id Real Complex Real.instCommSemiring instSemiring Algebra.complexToReal Algebra.id instCommSemiring AlgHomClass.toAlgHom AlgEquiv AlgEquiv.instFunLike AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass conjAe	—	AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass algHom_ext conj_I eq_or_eq_neg_of_sq_eq_sq IsDomain.to_noZeroDivisors Field.isDomain map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass I_sq map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass map_one MonoidHomClass.toOneHomClass
selfAdjointEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex AddSubgroup AddGroupWithOne.toAddGroup addGroupWithOne SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing instStarRing NonUnitalNonAssocSemiring.toAddCommMonoid selfAdjoint.instCommRingSubtypeMemAddSubgroup Real.instAddCommMonoid selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid Real.commRing instStarRingReal instTrivialStarReal addCommGroup Module.complexToReal Semiring.toModule instSemiring instStarModuleReal EquivLike.toFunLike LinearEquiv.instEquivLike selfAdjointEquiv re	—	RingHomInvPair.ids instTrivialStarReal instStarModuleReal
selfAdjointEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex AddSubgroup AddGroupWithOne.toAddGroup addGroupWithOne SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing instStarRing Real.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid selfAdjoint.instCommRingSubtypeMemAddSubgroup Semiring.toModule selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid Real.commRing instStarRingReal instTrivialStarReal addCommGroup Module.complexToReal instSemiring instStarModuleReal EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm selfAdjointEquiv ofReal conj_ofReal	—	RingHomInvPair.ids instTrivialStarReal instStarModuleReal
toMatrix_conjAe 📖	mathematical	—	DFunLike.coe LinearEquiv Real CommSemiring.toSemiring Real.instCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Complex NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing Algebra.toModule instSemiring instAlgebraOfReal Algebra.id Matrix LinearMap.addCommMonoid Matrix.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix Fin.fintype Finite.of_fintype basisOneI AlgEquiv.toLinearMap Algebra.complexToReal instCommSemiring conjAe Equiv Equiv.instEquivLike Matrix.of Matrix.vecCons Real.instOne Real.instZero Matrix.vecEmpty Real.instNeg	—	Matrix.ext RingHomInvPair.ids smulCommClass_self Finite.of_fintype Fintype.complete LinearMap.toMatrix_apply coe_basisOneI map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Matrix.cons_val' Matrix.cons_val_fin_one conj_I map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass neg_zero

ComplexStarModule

Definitions

Name	Category	Theorems
termℑ 📖	CompOp	—
termℜ 📖	CompOp	—

IsScalarTower

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
complexToReal 📖	mathematical	—	IsScalarTower Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid Module.complexToReal	—	smul_assoc

IsSelfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_realPart 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing StarRing.toStarAddMonoid instStarRingReal instTrivialStarReal StarModule.complexToReal LinearMap.instFunLike realPart	—	coe_selfAdjointPart_apply instTrivialStarReal StarModule.complexToReal IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing
imaginaryPart 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddSubgroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing StarRing.toStarAddMonoid instStarRingReal instTrivialStarReal StarModule.complexToReal LinearMap.instFunLike imaginaryPart AddSubgroup.zero	—	instTrivialStarReal StarModule.complexToReal imaginaryPart.eq_1 LinearMap.comp_apply skewAdjointPart_apply map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass

Module

Definitions

Name	Category	Theorems
complexToReal 📖	CompOp	63 math math: Complex.coe_realPart, IsSelfAdjoint.quasispectrumRestricts, realPart_idem, realPart_ofReal, imaginaryPart_I_smul, Complex.reLm_coe, Complex.instFiniteDimensionalReal, isSelfAdjoint_iff_isStarNormal_and_spectrumRestricts, CStarModule.inner_smul_right_real, FiniteDimensional.complexToReal, selfAdjoint.imaginaryPart_coe, realPart.norm_le, realPart_add_I_smul_imaginaryPart, cfcₙ_real_eq_complex, IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus, Complex.selfAdjointEquiv_apply, SMulCommClass.complexToReal, Complex.equivRealProdLm_apply, CStarAlgebra.linear_combination_nonneg, CStarAlgebra.norm_smul_two_inv_smul_add_four_unitary, star_mul_self_add_self_mul_star, imaginaryPart.norm_le, realPart_comp_subtype_selfAdjoint, skewAdjoint.negISMul_apply_coe, Complex.rank_real_complex', imaginaryPart_realPart, QuasispectrumRestricts.real_iff, imaginaryPart_eq_neg_I_smul_skewAdjointPart, Complex.equivRealProdLm_symm_apply, Complex.equivRealProdLm_symm_apply_im, realPart_I_smul, selfAdjoint.realPart_unitarySelfAddISMul, isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts, imaginaryPart_apply_coe, imaginaryPart_comp_subtype_selfAdjoint, realPart_surjective, imaginaryPart_surjective, selfAdjoint.realPart_coe, CStarModule.inner_smul_left_real, cfcₙHom_real_eq_restrict, Complex.equivRealProdLm_symm_apply_re, StarModule.complexToReal, Complex.coe_selfAdjointEquiv, imaginaryPart_ofReal, finrank_real_of_complex, Complex.coe_smul, Complex.selfAdjointEquiv_symm_apply, Complex.finrank_real_complex, Complex.finrank_real_complex_fact, realPart_imaginaryPart, rank_real_of_complex, IsScalarTower.complexToReal, skewAdjointPart_eq_I_smul_imaginaryPart, imaginaryPart_imaginaryPart, imaginaryPart_smul, realPart_apply_coe, IsSelfAdjoint.coe_realPart, realPart_smul, skewAdjoint.I_smul_neg_I, IsSelfAdjoint.imaginaryPart, Complex.imLm_coe, cfcₙ_complex_eq_real, Complex.rank_real_complex

SMulCommClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
complexToReal 📖	mathematical	—	SMulCommClass Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid Module.complexToReal	—	smul_comm

StarModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
complexToReal 📖	mathematical	—	StarModule Real InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing StarRing.toStarAddMonoid instStarRingReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid Module.complexToReal	—	smul_one_smul IsScalarTower.complexToReal IsScalarTower.left star_smul Complex.instStarModuleReal star_one

(root)

Definitions

Name	Category	Theorems
imaginaryPart 📖	CompOp	20 math math: imaginaryPart_I_smul, selfAdjoint.imaginaryPart_coe, realPart_add_I_smul_imaginaryPart, CStarAlgebra.linear_combination_nonneg, CStarAlgebra.norm_smul_two_inv_smul_add_four_unitary, star_mul_self_add_self_mul_star, imaginaryPart.norm_le, imaginaryPart_realPart, imaginaryPart_eq_neg_I_smul_skewAdjointPart, realPart_I_smul, imaginaryPart_apply_coe, imaginaryPart_comp_subtype_selfAdjoint, imaginaryPart_surjective, imaginaryPart_ofReal, realPart_imaginaryPart, skewAdjointPart_eq_I_smul_imaginaryPart, imaginaryPart_imaginaryPart, imaginaryPart_smul, realPart_smul, IsSelfAdjoint.imaginaryPart
realPart 📖	CompOp	20 math math: Complex.coe_realPart, realPart_idem, realPart_ofReal, imaginaryPart_I_smul, realPart.norm_le, realPart_add_I_smul_imaginaryPart, CStarAlgebra.linear_combination_nonneg, CStarAlgebra.norm_smul_two_inv_smul_add_four_unitary, star_mul_self_add_self_mul_star, realPart_comp_subtype_selfAdjoint, imaginaryPart_realPart, realPart_I_smul, selfAdjoint.realPart_unitarySelfAddISMul, realPart_surjective, selfAdjoint.realPart_coe, realPart_imaginaryPart, imaginaryPart_smul, realPart_apply_coe, IsSelfAdjoint.coe_realPart, realPart_smul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
imaginaryPart_I_smul 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing StarRing.toStarAddMonoid instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike imaginaryPart Complex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction Complex.I realPart	—	instTrivialStarReal StarModule.complexToReal Nat.instAtLeastTwoHAddOfNat imaginaryPart_apply_coe StarModule.star_smul Complex.conj_I neg_smul sub_neg_eq_add smul_add SMulCommClass.smul_comm IsScalarTower.to_smulCommClass' IsScalarTower.complexToReal IsScalarTower.left smul_smul Complex.I_mul_I one_smul smul_neg neg_neg realPart_apply_coe
imaginaryPart_apply_coe 📖	mathematical	—	AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing StarRing.toStarAddMonoid instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike imaginaryPart Complex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction Complex.instNeg Complex.I Real.instMonoid Real.instInv instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat SubNegMonoid.toSub Star.star	—	instTrivialStarReal StarModule.complexToReal Nat.instAtLeastTwoHAddOfNat invOf_eq_inv neg_smul
imaginaryPart_comp_subtype_selfAdjoint 📖	mathematical	—	LinearMap.comp Real Submodule Real.semiring AddCommGroup.toAddCommMonoid Module.complexToReal SetLike.instMembership Submodule.setLike selfAdjoint.submodule StarRing.toStarMul NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instStarRingReal instTrivialStarReal StarModule.complexToReal InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddSubgroup AddSubgroup.instSetLike selfAdjoint Submodule.addCommMonoid AddSubgroup.toAddCommGroup Submodule.module selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing StarRing.toStarAddMonoid RingHom.id RingHomCompTriple.ids imaginaryPart Submodule.subtype LinearMap LinearMap.instZero	—	instTrivialStarReal StarModule.complexToReal RingHomCompTriple.ids imaginaryPart.eq_1 LinearMap.comp_assoc skewAdjointPart_comp_subtype_selfAdjoint LinearMap.comp_zero
imaginaryPart_eq_neg_I_smul_skewAdjointPart 📖	mathematical	—	AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing StarRing.toStarAddMonoid instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike imaginaryPart Complex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction Complex.instNeg Complex.I skewAdjoint skewAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule StarMul.toInvolutiveStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring StarRing.toStarMul skewAdjointPart invertibleTwo Semifield.toDivisionSemiring Field.toSemifield Real.instField IsStrictOrderedRing.toCharZero DivisionSemiring.toSemiring Real.partialOrder Real.instIsStrictOrderedRing	—	instTrivialStarReal StarModule.complexToReal
imaginaryPart_imaginaryPart 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing StarRing.toStarAddMonoid instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike imaginaryPart AddSubgroup.zero	—	IsSelfAdjoint.imaginaryPart instTrivialStarReal StarModule.complexToReal
imaginaryPart_ofReal 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex AddSubgroup AddCommGroup.toAddGroup Complex.addCommGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Complex.commRing Complex.instStarRing AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal Semiring.toModule Complex.instSemiring selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid StarMul.toStarModule CommRing.toCommMonoid StarRing.toStarMul LinearMap.instFunLike imaginaryPart Complex.ofReal AddSubgroup.zero	—	instTrivialStarReal StarModule.complexToReal StarMul.toStarModule Nat.instAtLeastTwoHAddOfNat imaginaryPart_apply_coe Complex.conj_ofReal sub_self smul_zero MulZeroClass.mul_zero
imaginaryPart_realPart 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing StarRing.toStarAddMonoid instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike imaginaryPart realPart AddSubgroup.zero	—	IsSelfAdjoint.imaginaryPart instTrivialStarReal StarModule.complexToReal
imaginaryPart_smul 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing StarRing.toStarAddMonoid instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike imaginaryPart Complex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction AddSubgroup.add selfAdjoint.instSMulSubtypeMemAddSubgroupOfStarModule Real.instMonoid Complex.re Complex.im realPart	—	instTrivialStarReal StarModule.complexToReal Complex.re_add_im add_smul map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass imaginaryPart_I_smul
imaginaryPart_surjective 📖	mathematical	—	AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing StarRing.toStarAddMonoid instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike imaginaryPart	—	instTrivialStarReal StarModule.complexToReal imaginaryPart_I_smul IsSelfAdjoint.coe_realPart
realPart_I_smul 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing StarRing.toStarAddMonoid instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike realPart Complex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction Complex.I AddSubgroup.neg imaginaryPart	—	instTrivialStarReal StarModule.complexToReal Nat.instAtLeastTwoHAddOfNat realPart_apply_coe StarModule.star_smul Complex.conj_I neg_smul smul_add smul_neg imaginaryPart_apply_coe sub_eq_add_neg SMulCommClass.smul_comm IsScalarTower.to_smulCommClass' IsScalarTower.complexToReal IsScalarTower.left neg_neg neg_add_rev add_comm
realPart_add_I_smul_imaginaryPart 📖	mathematical	—	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddSubgroup.toAddCommGroup Module.complexToReal selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing StarRing.toStarAddMonoid instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike realPart Complex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction Complex.I imaginaryPart	—	instTrivialStarReal StarModule.complexToReal Nat.instAtLeastTwoHAddOfNat realPart_apply_coe smul_add imaginaryPart_apply_coe smul_sub neg_smul neg_sub_neg smul_smul Complex.I_mul_I one_smul add_add_sub_cancel IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing invOf_eq_inv invOf_two_smul_add_invOf_two_smul
realPart_apply_coe 📖	mathematical	—	AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing StarRing.toStarAddMonoid instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike realPart SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.instInv instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Star.star	—	instTrivialStarReal StarModule.complexToReal Nat.instAtLeastTwoHAddOfNat invOf_eq_inv
realPart_comp_subtype_selfAdjoint 📖	mathematical	—	LinearMap.comp Real Submodule Real.semiring AddCommGroup.toAddCommMonoid Module.complexToReal SetLike.instMembership Submodule.setLike selfAdjoint.submodule StarRing.toStarMul NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instStarRingReal instTrivialStarReal StarModule.complexToReal InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddSubgroup AddSubgroup.instSetLike selfAdjoint Submodule.addCommMonoid AddSubgroup.toAddCommGroup Submodule.module selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing StarRing.toStarAddMonoid RingHom.id RingHomCompTriple.ids realPart Submodule.subtype LinearMap.id	—	selfAdjointPart_comp_subtype_selfAdjoint instTrivialStarReal IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing
realPart_idem 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing StarRing.toStarAddMonoid instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike realPart	—	instTrivialStarReal StarModule.complexToReal IsSelfAdjoint.coe_realPart
realPart_imaginaryPart 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing StarRing.toStarAddMonoid instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike realPart imaginaryPart	—	instTrivialStarReal StarModule.complexToReal IsSelfAdjoint.coe_realPart
realPart_ofReal 📖	mathematical	—	Complex AddSubgroup AddCommGroup.toAddGroup Complex.addCommGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Complex.commRing Complex.instStarRing DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal Semiring.toModule Complex.instSemiring selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid StarMul.toStarModule CommRing.toCommMonoid StarRing.toStarMul LinearMap.instFunLike realPart Complex.ofReal	—	instTrivialStarReal StarModule.complexToReal StarMul.toStarModule Nat.instAtLeastTwoHAddOfNat realPart_apply_coe Complex.star_def Complex.conj_ofReal two_smul Complex.ofReal_inv inv_mul_cancel_left₀ Complex.instCharZero
realPart_smul 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing StarRing.toStarAddMonoid instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike realPart Complex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction AddSubgroup.sub selfAdjoint.instSMulSubtypeMemAddSubgroupOfStarModule Real.instMonoid Complex.re Complex.im imaginaryPart	—	instTrivialStarReal StarModule.complexToReal Complex.re_add_im sub_eq_add_neg add_smul map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass realPart_I_smul smul_neg
realPart_surjective 📖	mathematical	—	AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing StarRing.toStarAddMonoid instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike realPart	—	instTrivialStarReal StarModule.complexToReal IsSelfAdjoint.coe_realPart
skewAdjointPart_eq_I_smul_imaginaryPart 📖	mathematical	—	AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike skewAdjoint DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal skewAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarMul.toInvolutiveStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring StarRing.toStarMul instStarRingReal instTrivialStarReal StarModule.complexToReal StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike skewAdjointPart invertibleTwo Semifield.toDivisionSemiring Field.toSemifield Real.instField IsStrictOrderedRing.toCharZero DivisionSemiring.toSemiring Real.partialOrder Real.instIsStrictOrderedRing Complex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction Complex.I selfAdjoint selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing StarRing.toStarAddMonoid imaginaryPart	—	instTrivialStarReal StarModule.complexToReal IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat invOf_eq_inv imaginaryPart_apply_coe neg_smul smul_neg smul_smul Complex.I_mul_I one_smul neg_neg
span_selfAdjoint 📖	mathematical	—	Submodule.span Complex Complex.instSemiring AddCommGroup.toAddCommMonoid SetLike.coe AddSubgroup AddCommGroup.toAddGroup AddSubgroup.instSetLike selfAdjoint Top.top Submodule Submodule.instTop	—	Submodule.eq_top_iff' instTrivialStarReal StarModule.complexToReal realPart_add_I_smul_imaginaryPart AddMemClass.add_mem AddSubmonoidClass.toAddMemClass Submodule.addSubmonoidClass Submodule.subset_span SMulMemClass.smul_mem Submodule.smulMemClass
star_mul_self_add_self_mul_star 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Distrib.toMul Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup AddSubgroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal LinearMap.instFunLike realPart imaginaryPart	—	instTrivialStarReal StarModule.complexToReal realPart_add_I_smul_imaginaryPart StarAddMonoid.star_add selfAdjoint.star_val_eq StarModule.star_smul Complex.conj_I neg_smul mul_add Distrib.leftDistribClass add_mul Distrib.rightDistribClass neg_mul smul_mul_assoc mul_smul_comm smul_add smul_neg smul_smul Complex.I_mul_I one_smul neg_neg mul_neg neg_add_rev two_smul Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg add_zero Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Abel.zero_termg

selfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
imaginaryPart_coe 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing StarRing.toStarAddMonoid instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike imaginaryPart AddSubgroup.zero	—	IsSelfAdjoint.imaginaryPart
realPart_coe 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing StarRing.toStarAddMonoid instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike realPart	—	instTrivialStarReal StarModule.complexToReal IsSelfAdjoint.coe_realPart

skewAdjoint

Definitions

Name	Category	Theorems
negISMul 📖	CompOp	2 math math: negISMul_apply_coe, I_smul_neg_I

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
I_smul_neg_I 📖	mathematical	—	Complex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid Complex.I AddSubgroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring skewAdjoint AddSubgroup.toAddCommGroup instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing StarRing.toStarAddMonoid instStarRingReal instTrivialStarReal Module.complexToReal StarModule.complexToReal selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule LinearMap.instFunLike negISMul	—	instTrivialStarReal StarModule.complexToReal neg_smul smul_neg smul_smul Complex.I_mul_I one_smul neg_neg
negISMul_apply_coe 📖	mathematical	—	AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring skewAdjoint AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing StarRing.toStarAddMonoid instStarRingReal instTrivialStarReal Module.complexToReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule LinearMap.instFunLike negISMul Complex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction Complex.instNeg Complex.I	—	instTrivialStarReal StarModule.complexToReal

---

← Back to Index