Classes

📁 Source: Mathlib/Analysis/CStarAlgebra/Classes.lean

Statistics

Metric	Count
Definitions CStarAlgebra, toNonUnitalCStarAlgebra, toNormedAlgebra, toNormedRing, toStarRing, CommCStarAlgebra, toCStarAlgebra, toNonUnitalCommCStarAlgebra, toNormedAlgebra, toNormedCommRing, toStarRing, instCStarAlgebra, instCommCStarAlgebra, instNonUnitalCStarAlgebra, instNonUnitalCommCStarAlgebra, NonUnitalCStarAlgebra, toNonUnitalNormedRing, toNormedSpace, toStarRing, NonUnitalCommCStarAlgebra, toNonUnitalCStarAlgebra, toNonUnitalNormedCommRing, toNormedSpace, toStarRing, nonUnitalCStarAlgebra, nonUnitalCommCStarAlgebra, commCStarAlgebra, cstarAlgebra, instCStarAlgebraForall, instCStarAlgebraProd, instCStarAlgebraSubtypeMemStarSubalgebraComplexElemental, instCommCStarAlgebraComplex, instCommCStarAlgebraForall, instCommCStarAlgebraProd, instCommCStarAlgebraSubtypeMemStarSubalgebraComplexElementalOfIsStarNormal, instNonUnitalCStarAlgebraForall, instNonUnitalCStarAlgebraProd, instNonUnitalCStarAlgebraSubtypeMemNonUnitalStarSubalgebraComplexElemental, instNonUnitalCommCStarAlgebraForall, instNonUnitalCommCStarAlgebraProd, instNonUnitalCommCStarAlgebraSubtypeMemNonUnitalStarSubalgebraComplexElementalOfIsStarNormal	41
Theorems toCStarRing, toCompleteSpace, toStarModule, toCStarRing, toCompleteSpace, toStarModule, toCStarRing, toCompleteSpace, toIsScalarTower, toSMulCommClass, toStarModule, toCStarRing, toCompleteSpace, toIsScalarTower, toSMulCommClass, toStarModule	16
Total	57

CStarAlgebra

Definitions

Name	Category	Theorems
toNonUnitalCStarAlgebra 📖	CompOp	57 math math: Unitary.openPartialHomeomorph_source, IsStarNormal.spectralRadius_eq_nnnorm, PositiveLinearMap.apply_le_of_isSelfAdjoint, Unitary.mem_pathComponentOne_iff, selfAdjoint.expUnitaryPathToOne_apply, Unitary.continuousOn_argSelfAdjoint, StarAlgebra.elemental.characterSpaceToSpectrum_coe, mem_Icc_iff_nnnorm_le_one, Unitary.openPartialHomeomorph_symm_apply, Unitary.norm_sub_one_lt_two_iff, nnnorm_le_iff_of_nonneg, IsSelfAdjoint.neg_algebraMap_norm_le_self, unitary.norm_sub_eq, StarAlgebra.elemental.bijective_characterSpaceToSpectrum, Unitary.norm_sub_one_sq_eq, instNonnegSpectrumClass, norm_smul_two_inv_smul_add_four_unitary, CFC.monotone_rpow, nnnorm_le_one_iff_of_nonneg, unitary.two_mul_one_sub_le_norm_sub_one_sq, PositiveLinearMap.gnsStarAlgHom_apply, mem_Icc_algebraMap_iff_nnnorm_le, Unitary.openPartialHomeomorph_target, CFC.rpow_le_rpow, Unitary.spectrum_subset_slitPlane_iff_norm_lt_two, rpow_neg_one_le_rpow_neg_one, Unitization.nnreal_cfcₙ_eq_cfc_inr, IsSelfAdjoint.spectralRadius_eq_nnnorm, WStarAlgebra.exists_predual, Unitary.two_mul_one_sub_le_norm_sub_one_sq, rpow_neg_one_le_one, Unitary.norm_sub_eq, selfAdjoint.val_re_map_spectrum, PositiveLinearMap.norm_apply_le_of_nonneg, IsSelfAdjoint.self_add_I_smul_cfcSqrt_sub_sq_mem_unitary, unitary.norm_sub_one_lt_two_iff, unitary.norm_sub_one_sq_eq, StarAlgebra.elemental.continuous_characterSpaceToSpectrum, unitary.norm_argSelfAdjoint_le_pi, Unitary.norm_argSelfAdjoint_le_pi, Unitary.openPartialHomeomorph_apply, instNonnegSpectrumClassComplexUnital, Unitary.argSelfAdjoint_coe, exists_sum_four_unitary, cfcHom_eq_of_isStarNormal, unitary.mem_pathComponentOne_iff, continuousFunctionalCalculus_map_id, nnnorm_le_natCast_iff_of_nonneg, CFC.conjugate_rpow_neg_one_half, span_unitary, le_iff_norm_sqrt_mul_rpow, nnnorm_mem_spectrum_of_nonneg, WeakDual.CharacterSpace.instStarHomClass, selfAdjoint.joined_one_expUnitary, le_iff_norm_sqrt_mul_sqrt_inv, unitary.continuousOn_argSelfAdjoint, unitary.spectrum_subset_slitPlane_iff_norm_lt_two
toNormedAlgebra 📖	CompOp	81 math math: unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le, IsStarNormal.spectralRadius_eq_nnnorm, Unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le, mem_Icc_algebraMap_iff_norm_le, PositiveLinearMap.apply_le_of_isSelfAdjoint, CFC.tendsto_cfc_rpow_sub_one_log, Unitary.mem_pathComponentOne_iff, selfAdjoint.expUnitaryPathToOne_apply, selfAdjoint.norm_sq_expUnitary_sub_one, norm_or_neg_norm_mem_spectrum, StarAlgebra.elemental.characterSpaceToSpectrum_coe, gelfandStarTransform_naturality, gelfandStarTransform_apply_apply, ModularForm.tsum_logDeriv_eta_q, gelfandTransform_bijective, Unitary.openPartialHomeomorph_symm_apply, Unitary.norm_sub_one_lt_two_iff, nnnorm_le_iff_of_nonneg, IsSelfAdjoint.neg_algebraMap_norm_le_self, gelfandStarTransform_symm_apply, Unitary.expUnitary_eq_mul_inv, IsSelfAdjoint.val_re_map_spectrum, IsSelfAdjoint.isConnected_spectrum_compl, StarAlgebra.elemental.bijective_characterSpaceToSpectrum, gelfandTransform_map_star, selfAdjoint.unitarySelfAddISMul_coe, IsSelfAdjoint.cfc_arg, StarSubalgebra.spectrum_eq, ModularForm.logDeriv_one_sub_mul_cexp_comp, norm_smul_two_inv_smul_add_four_unitary, CFC.log_monotoneOn, IsSelfAdjoint.toReal_spectralRadius_complex_eq_norm, CFC.monotone_rpow, IsSelfAdjoint.sq_spectrumRestricts, ModularForm.logDeriv_eta_eq_E2, PositiveLinearMap.gnsStarAlgHom_apply, mem_Icc_algebraMap_iff_nnnorm_le, CFC.rpow_le_rpow, ModularForm.logDeriv_one_sub_cexp, expUnitary_argSelfAdjoint, Unitary.spectrum_subset_slitPlane_iff_norm_lt_two, selfAdjoint.star_coe_unitarySelfAddISMul, argSelfAdjoint_expUnitary, rpow_neg_one_le_rpow_neg_one, mul_star_le_algebraMap_norm_sq, IsSelfAdjoint.instIsometricContinuousFunctionalCalculus, norm_le_iff_le_algebraMap, IsSelfAdjoint.spectralRadius_eq_nnnorm, ModularForm.summable_logDeriv_one_sub_eta_q, IsStarNormal.instContinuousFunctionalCalculus, star_mul_le_algebraMap_norm_sq, StarSubalgebra.mem_spectrum_iff, rpow_neg_one_le_one, IsSelfAdjoint.map_spectrum_real, StarSubalgebra.coe_isUnit, selfAdjoint.val_re_map_spectrum, CFC.log_le_log, unitary.expUnitary_eq_mul_inv, IsSelfAdjoint.toReal_spectralRadius_eq_norm, IsSelfAdjoint.self_add_I_smul_cfcSqrt_sub_sq_mem_unitary, unitary.norm_sub_one_lt_two_iff, gelfandTransform_isometry, StarAlgebra.elemental.continuous_characterSpaceToSpectrum, norm_mem_spectrum_of_nonneg, toStarModule, IsStarNormal.instIsometricContinuousFunctionalCalculus, Unitary.argSelfAdjoint_coe, ModularForm.logDeriv_qParam, exists_sum_four_unitary, IsSelfAdjoint.le_algebraMap_norm_self, cfcHom_eq_of_isStarNormal, unitary.mem_pathComponentOne_iff, continuousFunctionalCalculus_map_id, CFC.conjugate_rpow_neg_one_half, le_iff_norm_sqrt_mul_rpow, Unitary.path_apply, nnnorm_mem_spectrum_of_nonneg, SpectrumRestricts.nnreal_iff_nnnorm, selfAdjoint.joined_one_expUnitary, le_iff_norm_sqrt_mul_sqrt_inv, unitary.spectrum_subset_slitPlane_iff_norm_lt_two
toNormedRing 📖	CompOp	57 math math: Unitary.openPartialHomeomorph_source, IsStarNormal.spectralRadius_eq_nnnorm, mem_Icc_algebraMap_iff_norm_le, AlgHomClass.instStarHomClass, Unitary.mem_pathComponentOne_iff, selfAdjoint.expUnitaryPathToOne_apply, Unitary.continuousOn_argSelfAdjoint, StarAlgebra.elemental.characterSpaceToSpectrum_coe, mem_Icc_iff_norm_le_one, gelfandStarTransform_naturality, mem_Icc_iff_nnnorm_le_one, gelfandTransform_bijective, Unitary.openPartialHomeomorph_symm_apply, spectrum.gelfandTransform_eq, unitary.norm_sub_eq, toCompleteSpace, Unitary.instLocPathConnectedSpace, StarAlgebra.elemental.bijective_characterSpaceToSpectrum, gelfandTransform_map_star, IsSelfAdjoint.cfc_arg, StarSubalgebra.spectrum_eq, norm_smul_two_inv_smul_add_four_unitary, CFC.log_monotoneOn, CFC.monotone_rpow, PositiveLinearMap.gnsStarAlgHom_apply, mem_Icc_algebraMap_iff_nnnorm_le, Unitary.openPartialHomeomorph_target, CFC.rpow_le_rpow, mul_star_le_algebraMap_norm_sq, IsSelfAdjoint.instIsometricContinuousFunctionalCalculus, IsStarNormal.instContinuousFunctionalCalculus, toCStarRing, star_mul_le_algebraMap_norm_sq, StarSubalgebra.mem_spectrum_iff, Unitary.isPathConnected_ball, Unitary.norm_sub_eq, StarSubalgebra.coe_isUnit, selfAdjoint.val_re_map_spectrum, Unitization.complex_cfcₙ_eq_cfc_inr, WeakDual.Complex.instStarHomClass, gelfandTransform_isometry, unitary.isPathConnected_ball, StarAlgebra.elemental.continuous_characterSpaceToSpectrum, unitary.norm_argSelfAdjoint_le_pi, Unitary.norm_argSelfAdjoint_le_pi, toStarModule, IsStarNormal.instIsometricContinuousFunctionalCalculus, Unitary.openPartialHomeomorph_apply, Unitary.argSelfAdjoint_coe, exists_sum_four_unitary, cfcHom_eq_of_isStarNormal, unitary.mem_pathComponentOne_iff, continuousFunctionalCalculus_map_id, span_unitary, WeakDual.CharacterSpace.instStarHomClass, selfAdjoint.joined_one_expUnitary, unitary.continuousOn_argSelfAdjoint
toStarRing 📖	CompOp	57 math math: Unitary.openPartialHomeomorph_source, AlgHomClass.instStarHomClass, CFC.tendsto_cfc_rpow_sub_one_log, Unitary.mem_pathComponentOne_iff, selfAdjoint.expUnitaryPathToOne_apply, Unitary.continuousOn_argSelfAdjoint, StarAlgebra.elemental.characterSpaceToSpectrum_coe, gelfandStarTransform_naturality, gelfandStarTransform_apply_apply, Unitary.openPartialHomeomorph_symm_apply, gelfandStarTransform_symm_apply, unitary.norm_sub_eq, Unitary.instLocPathConnectedSpace, StarAlgebra.elemental.bijective_characterSpaceToSpectrum, gelfandTransform_map_star, IsSelfAdjoint.cfc_arg, StarSubalgebra.spectrum_eq, norm_smul_two_inv_smul_add_four_unitary, CFC.log_monotoneOn, CFC.monotone_rpow, PositiveLinearMap.gnsStarAlgHom_apply, Unitary.openPartialHomeomorph_target, CFC.rpow_le_rpow, rpow_neg_one_le_rpow_neg_one, mul_star_le_algebraMap_norm_sq, IsSelfAdjoint.instIsometricContinuousFunctionalCalculus, IsStarNormal.instContinuousFunctionalCalculus, toCStarRing, star_mul_le_algebraMap_norm_sq, StarSubalgebra.mem_spectrum_iff, Unitary.isPathConnected_ball, rpow_neg_one_le_one, Unitary.norm_sub_eq, StarSubalgebra.coe_isUnit, selfAdjoint.val_re_map_spectrum, Unitization.complex_cfcₙ_eq_cfc_inr, CFC.log_le_log, WeakDual.Complex.instStarHomClass, unitary.isPathConnected_ball, StarAlgebra.elemental.continuous_characterSpaceToSpectrum, unitary.norm_argSelfAdjoint_le_pi, Unitary.norm_argSelfAdjoint_le_pi, toStarModule, IsStarNormal.instIsometricContinuousFunctionalCalculus, Unitary.openPartialHomeomorph_apply, Unitary.argSelfAdjoint_coe, exists_sum_four_unitary, cfcHom_eq_of_isStarNormal, unitary.mem_pathComponentOne_iff, continuousFunctionalCalculus_map_id, CFC.conjugate_rpow_neg_one_half, span_unitary, le_iff_norm_sqrt_mul_rpow, WeakDual.CharacterSpace.instStarHomClass, selfAdjoint.joined_one_expUnitary, le_iff_norm_sqrt_mul_sqrt_inv, unitary.continuousOn_argSelfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toCStarRing 📖	mathematical	—	CStarRing NormedRing.toNonUnitalNormedRing toNormedRing toStarRing	—	—
toCompleteSpace 📖	mathematical	—	CompleteSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NormedRing.toMetricSpace toNormedRing	—	—
toStarModule 📖	mathematical	—	StarModule Complex InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing Complex.instNormedField StarRing.toStarAddMonoid Complex.instStarRing StarMul.toInvolutiveStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring NormedRing.toRing toNormedRing StarRing.toStarMul toStarRing Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField SeminormedRing.toRing NormedRing.toSeminormedRing NormedAlgebra.toAlgebra toNormedAlgebra	—	—

CommCStarAlgebra

Definitions

Name	Category	Theorems
toCStarAlgebra 📖	CompOp	13 math math: gelfandStarTransform_naturality, gelfandStarTransform_apply_apply, ModularForm.tsum_logDeriv_eta_q, gelfandTransform_bijective, spectrum.gelfandTransform_eq, gelfandStarTransform_symm_apply, gelfandTransform_map_star, ModularForm.logDeriv_one_sub_mul_cexp_comp, ModularForm.logDeriv_eta_eq_E2, ModularForm.logDeriv_one_sub_cexp, ModularForm.summable_logDeriv_one_sub_eta_q, gelfandTransform_isometry, ModularForm.logDeriv_qParam
toNonUnitalCommCStarAlgebra 📖	CompOp	35 math math: IsStarNormal.instNonUnitalContinuousFunctionalCalculus, Ideal.toCharacterSpace_apply_eq_zero_of_mem, AlgHomClass.instStarHomClass, summableLocallyUniformlyOn_iteratedDerivWithin_cexp, iteratedDerivWithin_tsum_cexp_eq, gelfandStarTransform_naturality, gelfandStarTransform_apply_apply, spectrum.gelfandTransform_eq, gelfandStarTransform_symm_apply, CStarModule.inner_smul_left_complex, StarAlgebra.elemental.bijective_characterSpaceToSpectrum, gelfandTransform_map_star, cfcₙ_real_eq_complex, IsSelfAdjoint.cfc_arg, cfcHom_real_eq_restrict, inr_comp_cfcₙHom_eq_cfcₙAux, instNonemptyElemWeakDualComplexCharacterSpaceOfNontrivial, contDiffOn_tsum_cexp, cfcₙHom_real_eq_restrict, WStarAlgebra.exists_predual, IsStarNormal.instContinuousFunctionalCalculus, WeakDual.CharacterSpace.mem_spectrum_iff_exists, IsStarNormal.instNonUnitalIsometricContinuousFunctionalCalculus, Unitization.complex_cfcₙ_eq_cfc_inr, WeakDual.Complex.instStarHomClass, cfc_real_eq_complex, StarAlgebra.elemental.continuous_characterSpaceToSpectrum, IsStarNormal.instIsometricContinuousFunctionalCalculus, WeakDual.CharacterSpace.exists_apply_eq_zero, cfcHom_eq_of_isStarNormal, summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp, continuousFunctionalCalculus_map_id, CFC.complex_exp_eq_normedSpace_exp, WeakDual.CharacterSpace.instStarHomClass, differentiableAt_iteratedDerivWithin_cexp
toNormedAlgebra 📖	CompOp	1 math math: toStarModule
toNormedCommRing 📖	CompOp	85 math math: IsSelfAdjoint.quasispectrumRestricts, Ideal.toCharacterSpace_apply_eq_zero_of_mem, EisensteinSeries.hasSum_e2Summand_symmetricIcc, tsum_eisSummand_eq_riemannZeta_mul_eisensteinSeries, summableLocallyUniformlyOn_iteratedDerivWithin_cexp, Unitization.real_cfcₙ_eq_cfc_inr, StarAlgebra.elemental.characterSpaceToSpectrum_coe, iteratedDerivWithin_tsum_cexp_eq, CStarModule.innerSL_apply, isSelfAdjoint_iff_isStarNormal_and_spectrumRestricts, gelfandStarTransform_naturality, gelfandStarTransform_apply_apply, ModularForm.tsum_logDeriv_eta_q, EisensteinSeries.summable_left_one_div_linear_sub_one_div_linear, CStarMatrix.toCLM_injective, toCStarRing, gelfandTransform_bijective, EisensteinSeries.e2Summand_summable, CStarMatrix.norm_def', CStarMatrix.inner_toCLM_conjTranspose_left, PositiveLinearMap.preGNS_norm_def, summable_eisSummand, CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM, spectrum.gelfandTransform_eq, EisensteinSeries.tsum_symmetricIco_linear_sub_linear_add_one_eq_zero, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply_coe, EisensteinSeries.G2_eq_tsum_symmetricIco, gelfandStarTransform_symm_apply, PositiveLinearMap.preGNS_inner_def, IsSelfAdjoint.isConnected_spectrum_compl, EisensteinSeries.tendsto_e2Summand_atTop_nhds_zero, VonNeumannAlgebra.centralizer_centralizer', StarAlgebra.elemental.bijective_characterSpaceToSpectrum, gelfandTransform_map_star, EisensteinSeries.hasSum_e2Summand_symmetricIco, EisensteinSeries.q_expansion_riemannZeta, VonNeumannAlgebra.mem_carrier, ModularForm.differentiableAt_eta_tprod, cfcHom_real_eq_restrict, CStarMatrix.toCLM_apply_single, IsSelfAdjoint.spectrumRestricts, CStarMatrix.toCLM_apply_eq_sum, toStarModule, CStarMatrix.toCLM_apply, PositiveLinearMap.gnsStarAlgHom_apply, isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts, instNonemptyElemWeakDualComplexCharacterSpaceOfNontrivial, ModularForm.differentiableAt_eta_of_mem_upperHalfPlaneSet, CStarMatrix.mul_entry_mul_eq_inner_toCLM, contDiffOn_tsum_cexp, EisensteinSeries.qExpansion_identity_pnat, Unitization.nnreal_cfcₙ_eq_cfc_inr, cfcₙHom_real_eq_restrict, EisensteinSeries.tsum_tsum_symmetricIco_sub_eq, ModularForm.summable_logDeriv_one_sub_eta_q, WStarAlgebra.exists_predual, EisensteinSeries.q_expansion_bernoulli, EisensteinSeries.tendsto_double_sum_S_act, WeakDual.CharacterSpace.mem_spectrum_iff_exists, EisensteinSeries.summable_e2Summand_symmetricIcc, VonNeumannAlgebra.coe_toStarSubalgebra, summable_prod_eisSummand, EisensteinSeries.G2_eq_tsum_cexp, EisensteinSeries.qExpansion_identity, tsum_eisSummand_eq_tsum_sigma_mul_cexp_pow, EisensteinSeries.tendsto_tsum_one_div_linear_sub_succ_eq, EisensteinSeries.summable_e2Summand_symmetricIco, EisensteinSeries.summable_right_one_div_linear_sub_one_div_linear_succ, gelfandTransform_isometry, StarAlgebra.elemental.continuous_characterSpaceToSpectrum, WeakDual.CharacterSpace.exists_apply_eq_zero, cfcHom_eq_of_isStarNormal, toCompleteSpace, summable_pow_mul_cexp, summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply, continuousFunctionalCalculus_map_id, EisensteinSeries.tsum_symmetricIco_tsum_eq_S_act, PositiveLinearMap.preGNS_norm_sq, WeakDual.CharacterSpace.instStarHomClass, CStarMatrix.norm_def, ModularForm.multipliableLocallyUniformlyOn_eta, CStarMatrix.inner_toCLM_conjTranspose_right, CStarMatrix.toCLM_apply_single_apply, EisensteinSeries.tsum_symmetricIco_tsum_sub_eq
toStarRing 📖	CompOp	2 math math: toCStarRing, toStarModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toCStarRing 📖	mathematical	—	CStarRing NormedRing.toNonUnitalNormedRing NormedCommRing.toNormedRing toNormedCommRing toStarRing	—	—
toCompleteSpace 📖	mathematical	—	CompleteSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NormedRing.toMetricSpace NormedCommRing.toNormedRing toNormedCommRing	—	—
toStarModule 📖	mathematical	—	StarModule Complex InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing Complex.instNormedField StarRing.toStarAddMonoid Complex.instStarRing StarMul.toInvolutiveStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing toNormedCommRing StarRing.toStarMul toStarRing Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField SeminormedRing.toRing NormedRing.toSeminormedRing NormedAlgebra.toAlgebra toNormedAlgebra	—	—

MulOpposite

Definitions

Name	Category	Theorems
instCStarAlgebra 📖	CompOp	—
instCommCStarAlgebra 📖	CompOp	—
instNonUnitalCStarAlgebra 📖	CompOp	—
instNonUnitalCommCStarAlgebra 📖	CompOp	—

NonUnitalCStarAlgebra

Definitions

Name	Category	Theorems
toNonUnitalNormedRing 📖	CompOp	153 math math: Unitary.openPartialHomeomorph_source, CStarAlgebra.preimage_inr_Icc_zero_one, CStarMatrix.norm_entry_le_norm, IsStarNormal.instNonUnitalContinuousFunctionalCalculus, IsStarNormal.spectralRadius_eq_nnnorm, CFC.monotoneOn_one_sub_one_add_inv, toStarModule, PositiveLinearMap.apply_le_of_isSelfAdjoint, CFC.monotone_nnrpow, StarAlgEquiv.norm_map, CStarAlgebra.inr_mem_Icc_iff_norm_le, Unitary.mem_pathComponentOne_iff, Unitization.real_cfcₙ_eq_cfc_inr, selfAdjoint.expUnitaryPathToOne_apply, Unitary.continuousOn_argSelfAdjoint, StarAlgebra.elemental.characterSpaceToSpectrum_coe, WithCStarModule.prod_norm_sq, CStarModule.innerSL_apply, CStarAlgebra.span_nonneg_inter_unitBall, WithCStarModule.inner_def, CStarMatrix.instIsUniformAddGroup, CStarAlgebra.mem_Icc_iff_nnnorm_le_one, toCStarRing, CStarMatrix.toCLM_injective, NonUnitalStarAlgHom.nnnorm_apply_le, CStarMatrix.instStarOrderedRing, Unitization.instStarOrderedRing, CStarMatrix.norm_def', CStarMatrix.inner_toCLM_conjTranspose_left, PositiveLinearMap.preGNS_norm_def, PositiveLinearMap.leftMulMapPreGNS_apply, CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM, Unitary.openPartialHomeomorph_symm_apply, CompletelyPositiveMap.instLinearMapClassComplex, Filter.IsIncreasingApproximateUnit.toIsApproximateUnit, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply_coe, Unitary.norm_sub_one_lt_two_iff, CStarAlgebra.nnnorm_le_iff_of_nonneg, PositiveLinearMap.instContinuousLinearMapClassComplexOfLinearMapClassOfOrderHomClass, Filter.IsIncreasingApproximateUnit.eventually_nonneg, IsSelfAdjoint.neg_algebraMap_norm_le_self, gelfandStarTransform_symm_apply, unitary.norm_sub_eq, Filter.IsIncreasingApproximateUnit.eventually_norm, CStarAlgebra.instOrderClosedTopology, PositiveLinearMap.preGNS_inner_def, CStarAlgebra.instNonnegSpectrumClassComplexNonUnital, CStarAlgebra.span_nonneg_inter_unitClosedBall, StarAlgebra.elemental.bijective_characterSpaceToSpectrum, Filter.IsIncreasingApproximateUnit.eventually_nnnorm, PositiveLinearMap.toPreGNS_ofPreGNS, Unitary.norm_sub_one_sq_eq, PositiveLinearMap.exists_norm_apply_le, CStarAlgebra.instNonnegSpectrumClass, Filter.IsIncreasingApproximateUnit.eventually_isSelfAdjoint, CStarModule.norm_inner_le, CStarAlgebra.norm_smul_two_inv_smul_add_four_unitary, CStarMatrix.toCLM_apply_single, CStarMatrix.toCLM_apply_eq_sum, WithCStarModule.pi_norm, inr_comp_cfcₙHom_eq_cfcₙAux, CFC.monotoneOn_one_sub_one_add_inv_real, CStarMatrix.ofMatrix_eq_ofMatrixL, CStarAlgebra.nnnorm_le_one_iff_of_nonneg, CStarMatrix.instIsTopologicalAddGroup, unitary.two_mul_one_sub_le_norm_sub_one_sq, CStarMatrix.toCLM_apply, PositiveLinearMap.gnsStarAlgHom_apply, CStarAlgebra.mem_Icc_algebraMap_iff_nnnorm_le, NonUnitalStarAlgHom.nnnorm_map, Unitary.openPartialHomeomorph_target, WithCStarModule.pi_inner, WithCStarModule.prod_norm, NonUnitalStarAlgHom.norm_map, CStarMatrix.mul_entry_mul_eq_inner_toCLM, CStarModule.norm_sq_eq, Unitary.spectrum_subset_slitPlane_iff_norm_lt_two, WithCStarModule.inner_single_right, Unitization.nnreal_cfcₙ_eq_cfc_inr, CStarModule.norm_eq_csSup, IsSelfAdjoint.spectralRadius_eq_nnnorm, WStarAlgebra.exists_predual, CFC.nnrpow_le_nnrpow, CStarAlgebra.span_nonneg_inter_closedBall, CStarAlgebra.isClosed_nonneg, Unitary.two_mul_one_sub_le_norm_sub_one_sq, PositiveLinearMap.ofPreGNS_toPreGNS, Filter.IsIncreasingApproximateUnit.eventually_star_eq, CStarMatrix.normedSpaceCore, CStarModule.inner_mul_inner_swap_le, Unitary.norm_sub_eq, CFC.monotone_sqrt, NonUnitalStarAlgHom.isometry, CStarAlgebra.instNonnegSpectrumClass', norm_cfcₙ_one_sub_one_add_inv_lt_one, IsStarNormal.instNonUnitalIsometricContinuousFunctionalCalculus, toCompleteSpace, WithCStarModule.inner_single_left, CStarAlgebra.directedOn_nonneg_ball, PositiveLinearMap.leftMulMapPreGNS_mul_eq_comp, selfAdjoint.val_re_map_spectrum, Unitization.complex_cfcₙ_eq_cfc_inr, PositiveLinearMap.norm_apply_le_of_nonneg, toIsScalarTower, CFC.sqrt_le_sqrt, CStarModule.continuous_inner, StarAlgEquiv.nnnorm_map, PositiveLinearMap.instStarHomClassOfLinearMapClassComplexOfOrderHomClass, CStarAlgebra.spectralOrderedRing, IsSelfAdjoint.self_add_I_smul_cfcSqrt_sub_sq_mem_unitary, CStarMatrix.uniformEmbedding_ofMatrix, CStarAlgebra.inr_mem_Icc_iff_nnnorm_le, unitary.norm_sub_one_lt_two_iff, WithCStarModule.pi_norm_sq, unitary.norm_sub_one_sq_eq, CStarMatrix.instCStarRing, StarAlgebra.elemental.continuous_characterSpaceToSpectrum, unitary.norm_argSelfAdjoint_le_pi, CStarAlgebra.span_nonneg_inter_ball, CStarAlgebra.isBasis_nonneg_sections, Unitary.norm_argSelfAdjoint_le_pi, CFC.monotoneOn_cfcₙ_rpowIntegrand₀₁, Unitary.openPartialHomeomorph_apply, CStarAlgebra.instNonnegSpectrumClassComplexUnital, Unitary.argSelfAdjoint_coe, CStarAlgebra.hasBasis_approximateUnit, IsSelfAdjoint.instNonUnitalIsometricContinuousFunctionalCalculus, CStarAlgebra.exists_sum_four_unitary, cfcHom_eq_of_isStarNormal, NonUnitalStarAlgHom.norm_apply_le, WithCStarModule.prod_inner, unitary.mem_pathComponentOne_iff, toSMulCommClass, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply, continuousFunctionalCalculus_map_id, CStarAlgebra.nnnorm_le_natCast_iff_of_nonneg, CStarAlgebra.span_unitary, le_iff_norm_sqrt_mul_rpow, CStarAlgebra.nnnorm_mem_spectrum_of_nonneg, CStarAlgebra.exists_sum_four_nonneg, PositiveLinearMap.preGNS_norm_sq, WeakDual.CharacterSpace.instStarHomClass, Unitization.inr_nonneg_iff, CStarMatrix.norm_def, StarAlgEquiv.isometry, CStarMatrix.inner_toCLM_conjTranspose_right, NonUnitalStarAlgHom.instContinuousLinearMapClassComplex, CStarMatrix.toCLM_apply_single_apply, selfAdjoint.joined_one_expUnitary, Unitization.cfcₙ_eq_cfc_inr, le_iff_norm_sqrt_mul_sqrt_inv, unitary.continuousOn_argSelfAdjoint, unitary.spectrum_subset_slitPlane_iff_norm_lt_two
toNormedSpace 📖	CompOp	100 math math: IsStarNormal.instNonUnitalContinuousFunctionalCalculus, CFC.monotoneOn_one_sub_one_add_inv, toStarModule, PositiveLinearMap.apply_le_of_isSelfAdjoint, CFC.monotone_nnrpow, summableLocallyUniformlyOn_iteratedDerivWithin_cexp, Unitization.real_cfcₙ_eq_cfc_inr, StarAlgebra.elemental.characterSpaceToSpectrum_coe, iteratedDerivWithin_tsum_cexp_eq, WithCStarModule.prod_norm_sq, CStarModule.innerSL_apply, CStarAlgebra.span_nonneg_inter_unitBall, WithCStarModule.inner_def, gelfandStarTransform_naturality, gelfandStarTransform_apply_apply, CStarMatrix.toCLM_injective, Unitization.instStarOrderedRing, CStarMatrix.norm_def', CStarMatrix.inner_toCLM_conjTranspose_left, PositiveLinearMap.preGNS_norm_def, PositiveLinearMap.leftMulMapPreGNS_apply, CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM, CompletelyPositiveMap.instLinearMapClassComplex, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply_coe, PositiveLinearMap.instContinuousLinearMapClassComplexOfLinearMapClassOfOrderHomClass, gelfandStarTransform_symm_apply, PositiveLinearMap.preGNS_inner_def, CStarAlgebra.instNonnegSpectrumClassComplexNonUnital, CStarAlgebra.span_nonneg_inter_unitClosedBall, StarAlgebra.elemental.bijective_characterSpaceToSpectrum, selfAdjoint.unitarySelfAddISMul_coe, PositiveLinearMap.toPreGNS_ofPreGNS, PositiveLinearMap.exists_norm_apply_le, CStarAlgebra.instNonnegSpectrumClass, CStarModule.norm_inner_le, cfcHom_real_eq_restrict, CStarAlgebra.norm_smul_two_inv_smul_add_four_unitary, CStarMatrix.toCLM_apply_single, CStarMatrix.toCLM_apply_eq_sum, WithCStarModule.pi_norm, inr_comp_cfcₙHom_eq_cfcₙAux, CFC.monotoneOn_one_sub_one_add_inv_real, CStarMatrix.ofMatrix_eq_ofMatrixL, CStarMatrix.toCLM_apply, selfAdjoint.realPart_unitarySelfAddISMul, PositiveLinearMap.gnsStarAlgHom_apply, WithCStarModule.pi_inner, WithCStarModule.prod_norm, CStarMatrix.mul_entry_mul_eq_inner_toCLM, CStarModule.norm_sq_eq, contDiffOn_tsum_cexp, WithCStarModule.inner_single_right, selfAdjoint.star_coe_unitarySelfAddISMul, Unitization.nnreal_cfcₙ_eq_cfc_inr, CStarModule.norm_eq_csSup, cfcₙHom_real_eq_restrict, CStarAlgebra.conjugate_le_norm_smul', WStarAlgebra.exists_predual, CFC.nnrpow_le_nnrpow, CStarAlgebra.span_nonneg_inter_closedBall, CStarAlgebra.star_left_conjugate_le_norm_smul, PositiveLinearMap.ofPreGNS_toPreGNS, CStarMatrix.normedSpaceCore, CStarModule.inner_mul_inner_swap_le, CFC.monotone_sqrt, CStarAlgebra.instNonnegSpectrumClass', CStarAlgebra.conjugate_le_norm_smul, norm_cfcₙ_one_sub_one_add_inv_lt_one, IsStarNormal.instNonUnitalIsometricContinuousFunctionalCalculus, WithCStarModule.inner_single_left, Unitization.complex_cfcₙ_eq_cfc_inr, PositiveLinearMap.norm_apply_le_of_nonneg, toIsScalarTower, CFC.sqrt_le_sqrt, CStarModule.continuous_inner, IsSelfAdjoint.self_add_I_smul_cfcSqrt_sub_sq_mem_unitary, CompletelyPositiveMap.map_cstarMatrix_nonneg', WithCStarModule.pi_norm_sq, CStarAlgebra.star_right_conjugate_le_norm_smul, StarAlgebra.elemental.continuous_characterSpaceToSpectrum, CStarAlgebra.span_nonneg_inter_ball, CFC.monotoneOn_cfcₙ_rpowIntegrand₀₁, CStarAlgebra.instNonnegSpectrumClassComplexUnital, IsSelfAdjoint.instNonUnitalIsometricContinuousFunctionalCalculus, WithCStarModule.prod_inner, summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp, toSMulCommClass, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply, CStarAlgebra.span_unitary, le_iff_norm_sqrt_mul_rpow, CStarAlgebra.exists_sum_four_nonneg, PositiveLinearMap.preGNS_norm_sq, WeakDual.CharacterSpace.instStarHomClass, CStarMatrix.norm_def, differentiableAt_iteratedDerivWithin_cexp, CStarMatrix.inner_toCLM_conjTranspose_right, NonUnitalStarAlgHom.instContinuousLinearMapClassComplex, CStarMatrix.toCLM_apply_single_apply, Unitization.cfcₙ_eq_cfc_inr, le_iff_norm_sqrt_mul_sqrt_inv
toStarRing 📖	CompOp	49 math math: IsStarNormal.instNonUnitalContinuousFunctionalCalculus, CFC.monotoneOn_one_sub_one_add_inv, toStarModule, CFC.monotone_nnrpow, Unitization.real_cfcₙ_eq_cfc_inr, WithCStarModule.prod_norm_sq, CStarModule.innerSL_apply, WithCStarModule.inner_def, toCStarRing, CStarMatrix.instStarOrderedRing, Unitization.instStarOrderedRing, CStarMatrix.inner_toCLM_conjTranspose_left, PositiveLinearMap.preGNS_norm_def, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply_coe, PositiveLinearMap.preGNS_inner_def, Filter.IsIncreasingApproximateUnit.eventually_isSelfAdjoint, CStarModule.norm_inner_le, WithCStarModule.pi_norm, inr_comp_cfcₙHom_eq_cfcₙAux, CFC.monotoneOn_one_sub_one_add_inv_real, PositiveLinearMap.gnsStarAlgHom_apply, WithCStarModule.pi_inner, WithCStarModule.prod_norm, CStarMatrix.mul_entry_mul_eq_inner_toCLM, CStarModule.norm_sq_eq, WithCStarModule.inner_single_right, Unitization.nnreal_cfcₙ_eq_cfc_inr, CStarModule.norm_eq_csSup, CFC.nnrpow_le_nnrpow, Filter.IsIncreasingApproximateUnit.eventually_star_eq, CStarModule.inner_mul_inner_swap_le, CFC.monotone_sqrt, norm_cfcₙ_one_sub_one_add_inv_lt_one, IsStarNormal.instNonUnitalIsometricContinuousFunctionalCalculus, WithCStarModule.inner_single_left, Unitization.complex_cfcₙ_eq_cfc_inr, CFC.sqrt_le_sqrt, CStarModule.continuous_inner, PositiveLinearMap.instStarHomClassOfLinearMapClassComplexOfOrderHomClass, CStarAlgebra.spectralOrderedRing, WithCStarModule.pi_norm_sq, CStarMatrix.instCStarRing, CFC.monotoneOn_cfcₙ_rpowIntegrand₀₁, IsSelfAdjoint.instNonUnitalIsometricContinuousFunctionalCalculus, WithCStarModule.prod_inner, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply, PositiveLinearMap.preGNS_norm_sq, CStarMatrix.inner_toCLM_conjTranspose_right, Unitization.cfcₙ_eq_cfc_inr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toCStarRing 📖	mathematical	—	CStarRing toNonUnitalNormedRing toStarRing	—	—
toCompleteSpace 📖	mathematical	—	CompleteSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNormedRing.toMetricSpace toNonUnitalNormedRing	—	—
toIsScalarTower 📖	mathematical	—	IsScalarTower Complex SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Complex.instNormedField MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing toNonUnitalNormedRing Module.toDistribMulAction NormedSpace.toModule toNormedSpace SMulZeroClass.toSMul AddMonoid.toZero SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing DistribSMul.toSMulZeroClass AddSemigroup.toAdd AddMonoid.toAddSemigroup AddMonoid.zero_add AddMonoid.add_zero NonUnitalNonAssocSemiring.toDistribSMul AddCommGroup.add_comm NonUnitalNonAssocRing.toMul NonUnitalNonAssocRing.left_distrib NonUnitalNonAssocRing.right_distrib NonUnitalNonAssocRing.zero_mul NonUnitalNonAssocRing.mul_zero	—	—
toSMulCommClass 📖	mathematical	—	SMulCommClass Complex SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Complex.instNormedField MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing toNonUnitalNormedRing Module.toDistribMulAction NormedSpace.toModule toNormedSpace SMulZeroClass.toSMul AddMonoid.toZero SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing DistribSMul.toSMulZeroClass AddSemigroup.toAdd AddMonoid.toAddSemigroup AddMonoid.zero_add AddMonoid.add_zero NonUnitalNonAssocSemiring.toDistribSMul AddCommGroup.add_comm NonUnitalNonAssocRing.toMul NonUnitalNonAssocRing.left_distrib NonUnitalNonAssocRing.right_distrib NonUnitalNonAssocRing.zero_mul NonUnitalNonAssocRing.mul_zero	—	—
toStarModule 📖	mathematical	—	StarModule Complex InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing Complex.instNormedField StarRing.toStarAddMonoid Complex.instStarRing StarMul.toInvolutiveStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing toNonUnitalNormedRing AddCommGroup.add_comm NonUnitalNonAssocRing.toMul NonUnitalNonAssocRing.left_distrib NonUnitalNonAssocRing.right_distrib NonUnitalNonAssocRing.zero_mul NonUnitalNonAssocRing.mul_zero StarRing.toStarMul toStarRing SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing Module.toDistribMulAction NormedSpace.toModule toNormedSpace	—	—

NonUnitalCommCStarAlgebra

Definitions

Name	Category	Theorems
toNonUnitalCStarAlgebra 📖	CompOp	11 math math: summableLocallyUniformlyOn_iteratedDerivWithin_cexp, iteratedDerivWithin_tsum_cexp_eq, gelfandStarTransform_naturality, gelfandStarTransform_apply_apply, gelfandStarTransform_symm_apply, cfcHom_real_eq_restrict, contDiffOn_tsum_cexp, cfcₙHom_real_eq_restrict, WStarAlgebra.exists_predual, summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp, differentiableAt_iteratedDerivWithin_cexp
toNonUnitalNormedCommRing 📖	CompOp	33 math math: IsStarNormal.instNonUnitalContinuousFunctionalCalculus, Ideal.toCharacterSpace_apply_eq_zero_of_mem, AlgHomClass.instStarHomClass, gelfandStarTransform_naturality, gelfandStarTransform_apply_apply, spectrum.gelfandTransform_eq, gelfandStarTransform_symm_apply, CStarModule.inner_smul_left_complex, StarAlgebra.elemental.bijective_characterSpaceToSpectrum, gelfandTransform_map_star, cfcₙ_real_eq_complex, IsSelfAdjoint.cfc_arg, cfcHom_real_eq_restrict, toCompleteSpace, inr_comp_cfcₙHom_eq_cfcₙAux, instNonemptyElemWeakDualComplexCharacterSpaceOfNontrivial, toStarModule, toCStarRing, IsStarNormal.instContinuousFunctionalCalculus, WeakDual.CharacterSpace.mem_spectrum_iff_exists, IsStarNormal.instNonUnitalIsometricContinuousFunctionalCalculus, Unitization.complex_cfcₙ_eq_cfc_inr, WeakDual.Complex.instStarHomClass, toSMulCommClass, cfc_real_eq_complex, StarAlgebra.elemental.continuous_characterSpaceToSpectrum, IsStarNormal.instIsometricContinuousFunctionalCalculus, WeakDual.CharacterSpace.exists_apply_eq_zero, cfcHom_eq_of_isStarNormal, continuousFunctionalCalculus_map_id, CFC.complex_exp_eq_normedSpace_exp, WeakDual.CharacterSpace.instStarHomClass, toIsScalarTower
toNormedSpace 📖	CompOp	3 math math: toStarModule, toSMulCommClass, toIsScalarTower
toStarRing 📖	CompOp	2 math math: toStarModule, toCStarRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toCStarRing 📖	mathematical	—	CStarRing NonUnitalNormedCommRing.toNonUnitalNormedRing toNonUnitalNormedCommRing toStarRing	—	—
toCompleteSpace 📖	mathematical	—	CompleteSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNormedRing.toMetricSpace NonUnitalNormedCommRing.toNonUnitalNormedRing toNonUnitalNormedCommRing	—	—
toIsScalarTower 📖	mathematical	—	IsScalarTower Complex SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Complex.instNormedField MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalNormedCommRing.toNonUnitalNormedRing toNonUnitalNormedCommRing Module.toDistribMulAction NormedSpace.toModule toNormedSpace SMulZeroClass.toSMul AddMonoid.toZero SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing DistribSMul.toSMulZeroClass AddSemigroup.toAdd AddMonoid.toAddSemigroup AddMonoid.zero_add AddMonoid.add_zero NonUnitalNonAssocSemiring.toDistribSMul AddCommGroup.add_comm NonUnitalNonAssocRing.toMul NonUnitalNonAssocRing.left_distrib NonUnitalNonAssocRing.right_distrib NonUnitalNonAssocRing.zero_mul NonUnitalNonAssocRing.mul_zero	—	—
toSMulCommClass 📖	mathematical	—	SMulCommClass Complex SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Complex.instNormedField MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalNormedCommRing.toNonUnitalNormedRing toNonUnitalNormedCommRing Module.toDistribMulAction NormedSpace.toModule toNormedSpace SMulZeroClass.toSMul AddMonoid.toZero SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing DistribSMul.toSMulZeroClass AddSemigroup.toAdd AddMonoid.toAddSemigroup AddMonoid.zero_add AddMonoid.add_zero NonUnitalNonAssocSemiring.toDistribSMul AddCommGroup.add_comm NonUnitalNonAssocRing.toMul NonUnitalNonAssocRing.left_distrib NonUnitalNonAssocRing.right_distrib NonUnitalNonAssocRing.zero_mul NonUnitalNonAssocRing.mul_zero	—	—
toStarModule 📖	mathematical	—	StarModule Complex InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing Complex.instNormedField StarRing.toStarAddMonoid Complex.instStarRing StarMul.toInvolutiveStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing NonUnitalNormedCommRing.toNonUnitalNormedRing toNonUnitalNormedCommRing AddCommGroup.add_comm NonUnitalNonAssocRing.toMul NonUnitalNonAssocRing.left_distrib NonUnitalNonAssocRing.right_distrib NonUnitalNonAssocRing.zero_mul NonUnitalNonAssocRing.mul_zero StarRing.toStarMul toStarRing SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing Module.toDistribMulAction NormedSpace.toModule toNormedSpace	—	—

NonUnitalStarSubalgebra

Definitions

Name	Category	Theorems
nonUnitalCStarAlgebra 📖	CompOp	—
nonUnitalCommCStarAlgebra 📖	CompOp	—

StarSubalgebra

Definitions

Name	Category	Theorems
commCStarAlgebra 📖	CompOp	—
cstarAlgebra 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
CStarAlgebra 📖	CompData	—
CommCStarAlgebra 📖	CompData	—
NonUnitalCStarAlgebra 📖	CompData	—
NonUnitalCommCStarAlgebra 📖	CompData	—
instCStarAlgebraForall 📖	CompOp	—
instCStarAlgebraProd 📖	CompOp	—
instCStarAlgebraSubtypeMemStarSubalgebraComplexElemental 📖	CompOp	3 math math: StarAlgebra.elemental.characterSpaceToSpectrum_coe, StarAlgebra.elemental.bijective_characterSpaceToSpectrum, StarAlgebra.elemental.continuous_characterSpaceToSpectrum
instCommCStarAlgebraComplex 📖	CompOp	98 math math: IsStarNormal.instNonUnitalContinuousFunctionalCalculus, IsSelfAdjoint.quasispectrumRestricts, Ideal.toCharacterSpace_apply_eq_zero_of_mem, EisensteinSeries.hasSum_e2Summand_symmetricIcc, AlgHomClass.instStarHomClass, tsum_eisSummand_eq_riemannZeta_mul_eisensteinSeries, summableLocallyUniformlyOn_iteratedDerivWithin_cexp, Unitization.real_cfcₙ_eq_cfc_inr, StarAlgebra.elemental.characterSpaceToSpectrum_coe, iteratedDerivWithin_tsum_cexp_eq, CStarModule.innerSL_apply, isSelfAdjoint_iff_isStarNormal_and_spectrumRestricts, gelfandStarTransform_naturality, gelfandStarTransform_apply_apply, ModularForm.tsum_logDeriv_eta_q, EisensteinSeries.summable_left_one_div_linear_sub_one_div_linear, CStarMatrix.toCLM_injective, gelfandTransform_bijective, EisensteinSeries.e2Summand_summable, CStarMatrix.norm_def', CStarMatrix.inner_toCLM_conjTranspose_left, PositiveLinearMap.preGNS_norm_def, summable_eisSummand, CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM, spectrum.gelfandTransform_eq, EisensteinSeries.tsum_symmetricIco_linear_sub_linear_add_one_eq_zero, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply_coe, EisensteinSeries.G2_eq_tsum_symmetricIco, gelfandStarTransform_symm_apply, CStarModule.inner_smul_left_complex, PositiveLinearMap.preGNS_inner_def, IsSelfAdjoint.isConnected_spectrum_compl, EisensteinSeries.tendsto_e2Summand_atTop_nhds_zero, VonNeumannAlgebra.centralizer_centralizer', StarAlgebra.elemental.bijective_characterSpaceToSpectrum, gelfandTransform_map_star, cfcₙ_real_eq_complex, IsSelfAdjoint.cfc_arg, EisensteinSeries.hasSum_e2Summand_symmetricIco, EisensteinSeries.q_expansion_riemannZeta, VonNeumannAlgebra.mem_carrier, ModularForm.differentiableAt_eta_tprod, cfcHom_real_eq_restrict, CStarMatrix.toCLM_apply_single, IsSelfAdjoint.spectrumRestricts, CStarMatrix.toCLM_apply_eq_sum, inr_comp_cfcₙHom_eq_cfcₙAux, CStarMatrix.toCLM_apply, ModularForm.logDeriv_eta_eq_E2, PositiveLinearMap.gnsStarAlgHom_apply, isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts, instNonemptyElemWeakDualComplexCharacterSpaceOfNontrivial, ModularForm.differentiableAt_eta_of_mem_upperHalfPlaneSet, CStarMatrix.mul_entry_mul_eq_inner_toCLM, ModularForm.logDeriv_one_sub_cexp, contDiffOn_tsum_cexp, EisensteinSeries.qExpansion_identity_pnat, Unitization.nnreal_cfcₙ_eq_cfc_inr, cfcₙHom_real_eq_restrict, EisensteinSeries.tsum_tsum_symmetricIco_sub_eq, ModularForm.summable_logDeriv_one_sub_eta_q, WStarAlgebra.exists_predual, EisensteinSeries.q_expansion_bernoulli, IsStarNormal.instContinuousFunctionalCalculus, EisensteinSeries.tendsto_double_sum_S_act, WeakDual.CharacterSpace.mem_spectrum_iff_exists, EisensteinSeries.summable_e2Summand_symmetricIcc, IsStarNormal.instNonUnitalIsometricContinuousFunctionalCalculus, VonNeumannAlgebra.coe_toStarSubalgebra, summable_prod_eisSummand, EisensteinSeries.G2_eq_tsum_cexp, EisensteinSeries.qExpansion_identity, Unitization.complex_cfcₙ_eq_cfc_inr, tsum_eisSummand_eq_tsum_sigma_mul_cexp_pow, EisensteinSeries.tendsto_tsum_one_div_linear_sub_succ_eq, WeakDual.Complex.instStarHomClass, cfc_real_eq_complex, EisensteinSeries.summable_e2Summand_symmetricIco, EisensteinSeries.summable_right_one_div_linear_sub_one_div_linear_succ, gelfandTransform_isometry, StarAlgebra.elemental.continuous_characterSpaceToSpectrum, IsStarNormal.instIsometricContinuousFunctionalCalculus, ModularForm.logDeriv_qParam, WeakDual.CharacterSpace.exists_apply_eq_zero, cfcHom_eq_of_isStarNormal, summable_pow_mul_cexp, summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply, continuousFunctionalCalculus_map_id, EisensteinSeries.tsum_symmetricIco_tsum_eq_S_act, CFC.complex_exp_eq_normedSpace_exp, PositiveLinearMap.preGNS_norm_sq, WeakDual.CharacterSpace.instStarHomClass, CStarMatrix.norm_def, ModularForm.multipliableLocallyUniformlyOn_eta, CStarMatrix.inner_toCLM_conjTranspose_right, CStarMatrix.toCLM_apply_single_apply, EisensteinSeries.tsum_symmetricIco_tsum_sub_eq
instCommCStarAlgebraForall 📖	CompOp	—
instCommCStarAlgebraProd 📖	CompOp	—
instCommCStarAlgebraSubtypeMemStarSubalgebraComplexElementalOfIsStarNormal 📖	CompOp	—
instNonUnitalCStarAlgebraForall 📖	CompOp	—
instNonUnitalCStarAlgebraProd 📖	CompOp	—
instNonUnitalCStarAlgebraSubtypeMemNonUnitalStarSubalgebraComplexElemental 📖	CompOp	—
instNonUnitalCommCStarAlgebraForall 📖	CompOp	—
instNonUnitalCommCStarAlgebraProd 📖	CompOp	—
instNonUnitalCommCStarAlgebraSubtypeMemNonUnitalStarSubalgebraComplexElementalOfIsStarNormal 📖	CompOp	—

---

← Back to Index