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	76 math math: Unitary.openPartialHomeomorph_source, unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le, IsStarNormal.spectralRadius_eq_nnnorm, Unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le, PositiveLinearMap.apply_le_of_isSelfAdjoint, Unitary.mem_pathComponentOne_iff, selfAdjoint.expUnitaryPathToOne_apply, Unitary.continuousOn_argSelfAdjoint, selfAdjoint.norm_sq_expUnitary_sub_one, StarAlgebra.elemental.characterSpaceToSpectrum_coe, mem_Icc_iff_nnnorm_le_one, Unitization.sqrt_inr, Unitary.openPartialHomeomorph_symm_apply, Unitary.norm_sub_one_lt_two_iff, nnnorm_le_iff_of_nonneg, IsSelfAdjoint.neg_algebraMap_norm_le_self, Unitary.expUnitary_eq_mul_inv, unitary.norm_sub_eq, StarAlgebra.elemental.bijective_characterSpaceToSpectrum, selfAdjoint.unitarySelfAddISMul_coe, Unitary.norm_sub_one_sq_eq, instNonnegSpectrumClass, norm_smul_two_inv_smul_add_four_unitary, nnnorm_sub_mul_self_le, CFC.monotone_rpow, unitary.norm_argSelfAdjoint, nnnorm_le_one_iff_of_nonneg, unitary.two_mul_one_sub_le_norm_sub_one_sq, selfAdjoint.realPart_unitarySelfAddISMul, PositiveLinearMap.gnsStarAlgHom_apply, mem_Icc_algebraMap_iff_nnnorm_le, Unitary.openPartialHomeomorph_target, CFC.rpow_le_rpow, expUnitary_argSelfAdjoint, Unitary.spectrum_subset_slitPlane_iff_norm_lt_two, selfAdjoint.star_coe_unitarySelfAddISMul, argSelfAdjoint_expUnitary, 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, unitary.expUnitary_eq_mul_inv, PositiveLinearMap.norm_apply_le_of_nonneg, IsSelfAdjoint.self_add_I_smul_cfcSqrt_sub_sq_mem_unitary, Unitary.norm_argSelfAdjoint, norm_sub_mul_self_le, 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, Unitary.path_apply, nnnorm_mem_spectrum_of_nonneg, SpectrumRestricts.nnreal_iff_nnnorm, unitary.two_mul_one_sub_cos_norm_argSelfAdjoint, 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, Unitary.two_mul_one_sub_cos_norm_argSelfAdjoint
toNormedAlgebra 📖	CompOp	82 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, SpectrumRestricts.nnreal_add, selfAdjoint.joined_one_expUnitary, le_iff_norm_sqrt_mul_sqrt_inv, unitary.spectrum_subset_slitPlane_iff_norm_lt_two
toNormedRing 📖	CompOp	132 math math: Unitary.openPartialHomeomorph_source, 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, AlgHomClass.instStarHomClass, PositiveLinearMap.apply_le_of_isSelfAdjoint, CFC.tendsto_cfc_rpow_sub_one_log, Unitary.mem_pathComponentOne_iff, selfAdjoint.expUnitaryPathToOne_apply, Unitary.continuousOn_argSelfAdjoint, selfAdjoint.norm_sq_expUnitary_sub_one, norm_or_neg_norm_mem_spectrum, StarAlgebra.elemental.characterSpaceToSpectrum_coe, mem_Icc_iff_norm_le_one, pow_nonneg, norm_le_natCast_iff_of_nonneg, gelfandStarTransform_naturality, mem_Icc_iff_nnnorm_le_one, gelfandTransform_bijective, Unitary.openPartialHomeomorph_symm_apply, spectrum.gelfandTransform_eq, Unitary.norm_sub_one_lt_two_iff, nnnorm_le_iff_of_nonneg, isStrictlyPositive_add, IsSelfAdjoint.neg_algebraMap_norm_le_self, Unitary.expUnitary_eq_mul_inv, unitary.norm_sub_eq, IsSelfAdjoint.val_re_map_spectrum, toCompleteSpace, Unitary.instLocPathConnectedSpace, IsSelfAdjoint.isConnected_spectrum_compl, StarAlgebra.elemental.bijective_characterSpaceToSpectrum, gelfandTransform_map_star, selfAdjoint.unitarySelfAddISMul_coe, IsSelfAdjoint.cfc_arg, Unitary.norm_sub_one_sq_eq, inv_le_inv_iff, StarSubalgebra.spectrum_eq, norm_smul_two_inv_smul_add_four_unitary, SpectrumRestricts.eq_zero_of_neg, nnnorm_sub_mul_self_le, inv_le_one, CFC.log_monotoneOn, inv_le_iff, le_inv_iff, IsSelfAdjoint.toReal_spectralRadius_complex_eq_norm, CFC.monotone_rpow, inr_comp_cfcₙHom_eq_cfcₙAux, unitary.norm_argSelfAdjoint, nnnorm_le_one_iff_of_nonneg, unitary.two_mul_one_sub_le_norm_sub_one_sq, IsSelfAdjoint.sq_spectrumRestricts, selfAdjoint.realPart_unitarySelfAddISMul, PositiveLinearMap.gnsStarAlgHom_apply, mem_Icc_algebraMap_iff_nnnorm_le, Unitary.openPartialHomeomorph_target, CFC.rpow_le_rpow, unitary.joined, one_le_inv_iff_le_one, 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, inv_le_inv, norm_le_iff_le_algebraMap, isUnit_of_le, IsSelfAdjoint.spectralRadius_eq_nnnorm, Unitary.joined, le_one_of_one_le_inv, IsStarNormal.instContinuousFunctionalCalculus, toCStarRing, star_mul_le_algebraMap_norm_sq, pow_antitone, Unitary.two_mul_one_sub_le_norm_sub_one_sq, StarSubalgebra.mem_spectrum_iff, Unitary.isPathConnected_ball, rpow_neg_one_le_one, IsSelfAdjoint.map_spectrum_real, Unitary.norm_sub_eq, StarSubalgebra.coe_isUnit, pow_monotone, selfAdjoint.val_re_map_spectrum, Unitization.complex_cfcₙ_eq_cfc_inr, CFC.log_le_log, unitary.expUnitary_eq_mul_inv, PositiveLinearMap.norm_apply_le_of_nonneg, IsSelfAdjoint.toReal_spectralRadius_eq_norm, WeakDual.Complex.instStarHomClass, IsSelfAdjoint.self_add_I_smul_cfcSqrt_sub_sq_mem_unitary, Unitary.norm_argSelfAdjoint, norm_sub_mul_self_le, norm_le_one_iff_of_nonneg, unitary.norm_sub_one_lt_two_iff, gelfandTransform_isometry, unitary.isPathConnected_ball, unitary.norm_sub_one_sq_eq, StarAlgebra.elemental.continuous_characterSpaceToSpectrum, norm_mem_spectrum_of_nonneg, unitary.norm_argSelfAdjoint_le_pi, Unitary.norm_argSelfAdjoint_le_pi, toStarModule, IsStrictlyPositive.add_nonneg, IsStarNormal.instIsometricContinuousFunctionalCalculus, Unitary.openPartialHomeomorph_apply, Unitary.argSelfAdjoint_coe, IsStrictlyPositive.of_le, exists_sum_four_unitary, IsSelfAdjoint.le_algebraMap_norm_self, cfcHom_eq_of_isStarNormal, unitary.mem_pathComponentOne_iff, continuousFunctionalCalculus_map_id, nnnorm_le_natCast_iff_of_nonneg, CFC.conjugate_rpow_neg_one_half, inv_le_one_iff_one_le, span_unitary, le_iff_norm_sqrt_mul_rpow, Unitary.path_apply, nnnorm_mem_spectrum_of_nonneg, SpectrumRestricts.nnreal_iff_nnnorm, unitary.two_mul_one_sub_cos_norm_argSelfAdjoint, WeakDual.CharacterSpace.instStarHomClass, SpectrumRestricts.nnreal_add, IsStrictlyPositive.nonneg_add, selfAdjoint.joined_one_expUnitary, le_iff_norm_sqrt_mul_sqrt_inv, unitary.continuousOn_argSelfAdjoint, unitary.spectrum_subset_slitPlane_iff_norm_lt_two, Unitary.two_mul_one_sub_cos_norm_argSelfAdjoint
toStarRing 📖	CompOp	76 math math: Unitary.openPartialHomeomorph_source, unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le, Unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le, AlgHomClass.instStarHomClass, CFC.tendsto_cfc_rpow_sub_one_log, Unitary.mem_pathComponentOne_iff, selfAdjoint.expUnitaryPathToOne_apply, Unitary.continuousOn_argSelfAdjoint, selfAdjoint.norm_sq_expUnitary_sub_one, StarAlgebra.elemental.characterSpaceToSpectrum_coe, gelfandStarTransform_naturality, gelfandStarTransform_apply_apply, Unitary.openPartialHomeomorph_symm_apply, gelfandStarTransform_symm_apply, Unitary.expUnitary_eq_mul_inv, unitary.norm_sub_eq, Unitary.instLocPathConnectedSpace, StarAlgebra.elemental.bijective_characterSpaceToSpectrum, gelfandTransform_map_star, selfAdjoint.unitarySelfAddISMul_coe, IsSelfAdjoint.cfc_arg, StarSubalgebra.spectrum_eq, norm_smul_two_inv_smul_add_four_unitary, CFC.log_monotoneOn, CFC.monotone_rpow, inr_comp_cfcₙHom_eq_cfcₙAux, unitary.norm_argSelfAdjoint, selfAdjoint.realPart_unitarySelfAddISMul, PositiveLinearMap.gnsStarAlgHom_apply, Unitary.openPartialHomeomorph_target, CFC.rpow_le_rpow, unitary.joined, expUnitary_argSelfAdjoint, selfAdjoint.star_coe_unitarySelfAddISMul, argSelfAdjoint_expUnitary, rpow_neg_one_le_rpow_neg_one, mul_star_le_algebraMap_norm_sq, IsSelfAdjoint.instIsometricContinuousFunctionalCalculus, Unitary.joined, 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, unitary.expUnitary_eq_mul_inv, WeakDual.Complex.instStarHomClass, IsSelfAdjoint.self_add_I_smul_cfcSqrt_sub_sq_mem_unitary, Unitary.norm_argSelfAdjoint, 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, Unitary.path_apply, unitary.two_mul_one_sub_cos_norm_argSelfAdjoint, WeakDual.CharacterSpace.instStarHomClass, selfAdjoint.joined_one_expUnitary, le_iff_norm_sqrt_mul_sqrt_inv, unitary.continuousOn_argSelfAdjoint, Unitary.two_mul_one_sub_cos_norm_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	77 math math: cfc_realPart, IsStarNormal.instNonUnitalContinuousFunctionalCalculus, Ideal.toCharacterSpace_apply_eq_zero_of_mem, cfc_im_id, CFC.monotoneOn_one_sub_one_add_inv, AlgHomClass.instStarHomClass, CFC.monotone_nnrpow, CFC.tendsto_cfc_rpow_sub_one_log, summableLocallyUniformlyOn_iteratedDerivWithin_cexp, Unitization.real_cfcₙ_eq_cfc_inr, iteratedDerivWithin_tsum_cexp_eq, cfc_complex_eq_real, gelfandStarTransform_naturality, gelfandStarTransform_apply_apply, Unitization.sqrt_inr, ClosedSubmodule.inner_real_eq_re_inner, spectrum.gelfandTransform_eq, cfcₙ_re_id, gelfandStarTransform_symm_apply, CStarModule.inner_smul_left_complex, StarAlgebra.elemental.bijective_characterSpaceToSpectrum, gelfandTransform_map_star, cfcₙ_real_eq_complex, cfcₙ_comp_re, cfc_comp_im, IsSelfAdjoint.cfc_arg, cfcₙ_comp_im, cfcHom_real_eq_restrict, ClosedSubmodule.mem_symplComp_iff, CFC.log_monotoneOn, CFC.monotone_rpow, inr_comp_cfcₙHom_eq_cfcₙAux, CFC.monotoneOn_one_sub_one_add_inv_real, instNonemptyElemWeakDualComplexCharacterSpaceOfNontrivial, cfcₙ_imaginaryPart, CFC.rpow_le_rpow, cfc_comp_re, contDiffOn_tsum_cexp, selfAdjoint.star_coe_unitarySelfAddISMul, CStarAlgebra.rpow_neg_one_le_rpow_neg_one, cfcₙ_im_id, Unitization.nnreal_cfcₙ_eq_cfc_inr, cfcₙHom_real_eq_restrict, WStarAlgebra.exists_predual, CFC.nnrpow_le_nnrpow, IsStarNormal.instContinuousFunctionalCalculus, WeakDual.CharacterSpace.mem_spectrum_iff_exists, CStarAlgebra.rpow_neg_one_le_one, Derivative.normalizedDerivOfComplex_mdifferentiable, CFC.monotone_sqrt, norm_cfcₙ_one_sub_one_add_inv_lt_one, IsStarNormal.instNonUnitalIsometricContinuousFunctionalCalculus, Unitization.complex_cfcₙ_eq_cfc_inr, CFC.log_le_log, CFC.sqrt_le_sqrt, cfc_re_id, WeakDual.Complex.instStarHomClass, IsSelfAdjoint.self_add_I_smul_cfcSqrt_sub_sq_mem_unitary, cfcₙ_realPart, cfc_real_eq_complex, StarAlgebra.elemental.continuous_characterSpaceToSpectrum, CFC.monotoneOn_cfcₙ_rpowIntegrand₀₁, IsStarNormal.instIsometricContinuousFunctionalCalculus, WeakDual.CharacterSpace.exists_apply_eq_zero, E2_mdifferentiable, cfcHom_eq_of_isStarNormal, summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp, Derivative.serreDerivative_mdifferentiable, continuousFunctionalCalculus_map_id, CFC.conjugate_rpow_neg_one_half, CFC.complex_exp_eq_normedSpace_exp, le_iff_norm_sqrt_mul_rpow, cfcₙ_complex_eq_real, WeakDual.CharacterSpace.instStarHomClass, differentiableAt_iteratedDerivWithin_cexp, le_iff_norm_sqrt_mul_sqrt_inv, cfc_imaginaryPart
toNormedAlgebra 📖	CompOp	1 math math: toStarModule
toNormedCommRing 📖	CompOp	95 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, ModularForm.discriminant_bounded_factor, gelfandStarTransform_naturality, gelfandStarTransform_apply_apply, ModularForm.tsum_logDeriv_eta_q, EisensteinSeries.summable_left_one_div_linear_sub_one_div_linear, CStarMatrix.toCLM_injective, Unitization.sqrt_inr, toCStarRing, gelfandTransform_bijective, EisensteinSeries.e2Summand_summable, CStarMatrix.norm_def', ModularForm.discriminant_isZeroAtImInfty, 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, VonNeumannAlgebra.coe_mk, EisensteinSeries.hasSum_e2Summand_symmetricIco, EisensteinSeries.q_expansion_riemannZeta, VonNeumannAlgebra.mem_carrier, ModularForm.differentiableAt_eta_tprod, ModularForm.discriminant_eq_q_prod, ModularForm.logDeriv_one_sub_mul_cexp_comp, 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, SummableLocallyUniformlyOn.differentiableOn, EisensteinSeries.tendsto_double_sum_S_act, WeakDual.CharacterSpace.mem_spectrum_iff_exists, Derivative.normalizedDerivOfComplex_mdifferentiable, 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, E2_mdifferentiable, cfcHom_eq_of_isStarNormal, toCompleteSpace, summable_pow_mul_cexp, summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp, Derivative.serreDerivative_mdifferentiable, 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, differentiableAt_iteratedDerivWithin_cexp, 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	195 math math: Unitary.openPartialHomeomorph_source, CStarAlgebra.preimage_inr_Icc_zero_one, unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le, CStarMatrix.norm_entry_le_norm, IsStarNormal.instNonUnitalContinuousFunctionalCalculus, IsStarNormal.spectralRadius_eq_nnnorm, Unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le, 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, selfAdjoint.norm_sq_expUnitary_sub_one, StarAlgebra.elemental.characterSpaceToSpectrum_coe, WithCStarModule.prod_norm_sq, CStarModule.innerSL_apply, CStarAlgebra.span_nonneg_inter_unitBall, WithCStarModule.inner_def, CStarMatrix.instIsUniformAddGroup, CStarAlgebra.tendsto_mul_left_iff_tendsto_mul_right, CStarAlgebra.mem_Icc_iff_nnnorm_le_one, toCStarRing, CStarMatrix.toCLM_injective, Unitization.sqrt_inr, NonUnitalStarAlgHom.nnnorm_apply_le, CompletelyPositiveMapClass.map_cstarMatrix_nonneg', CStarMatrix.instStarOrderedRing, Unitization.instStarOrderedRing, CStarMatrix.norm_def', CStarMatrix.inner_toCLM_conjTranspose_left, IsStarProjection.conjugate_of_nonneg_of_le, CompletelyPositiveMap.map_cstarMatrix_nonneg, 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.expUnitary_eq_mul_inv, 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, Unitization.LE.le.of_inr, selfAdjoint.unitarySelfAddISMul_coe, 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, CStarAlgebra.nnnorm_sub_mul_self_le, CStarMatrix.toCLM_apply_eq_sum, WithCStarModule.pi_norm, inr_comp_cfcₙHom_eq_cfcₙAux, CFC.monotoneOn_one_sub_one_add_inv_real, unitary.norm_argSelfAdjoint, 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, IsStarProjection.le_tfae, selfAdjoint.realPart_unitarySelfAddISMul, PositiveLinearMap.gnsStarAlgHom_apply, IsStarProjection.le_iff_sub, CStarAlgebra.mem_Icc_algebraMap_iff_nnnorm_le, NonUnitalStarAlgHom.nnnorm_map, Unitary.openPartialHomeomorph_target, WithCStarModule.pi_inner, WithCStarModule.prod_norm, NonUnitalStarAlgHom.norm_map, IsStarProjection.le_iff_mul_eq_left, CStarMatrix.mul_entry_mul_eq_inner_toCLM, CStarModule.norm_sq_eq, expUnitary_argSelfAdjoint, Unitary.spectrum_subset_slitPlane_iff_norm_lt_two, WithCStarModule.inner_single_right, selfAdjoint.star_coe_unitarySelfAddISMul, argSelfAdjoint_expUnitary, Unitization.nnreal_cfcₙ_eq_cfc_inr, CStarModule.norm_eq_csSup, IsSelfAdjoint.spectralRadius_eq_nnnorm, IsStarProjection.mul_right_and_mul_left_of_nonneg_of_le, CStarAlgebra.conjugate_le_norm_smul', WStarAlgebra.exists_predual, CFC.nnrpow_le_nnrpow, CStarAlgebra.norm_le_norm_of_nonneg_of_le, CStarAlgebra.span_nonneg_inter_closedBall, CStarAlgebra.isClosed_nonneg, CStarAlgebra.star_left_conjugate_le_norm_smul, 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, IsStarProjection.commute_of_le, Unitary.norm_sub_eq, CFC.monotone_sqrt, NonUnitalStarAlgHom.isometry, CStarAlgebra.instNonnegSpectrumClass', CStarAlgebra.conjugate_le_norm_smul, 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, Unitization.LE.le.inr, unitary.expUnitary_eq_mul_inv, 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, Unitary.norm_argSelfAdjoint, CStarAlgebra.norm_sub_mul_self_le, CompletelyPositiveMap.map_cstarMatrix_nonneg', CStarMatrix.uniformEmbedding_ofMatrix, CStarAlgebra.inr_mem_Icc_iff_nnnorm_le, unitary.norm_sub_one_lt_two_iff, WithCStarModule.pi_norm_sq, CStarAlgebra.star_right_conjugate_le_norm_smul, unitary.norm_sub_one_sq_eq, CStarAlgebra.nnnorm_le_nnnorm_of_nonneg_of_le, 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, IsStarProjection.le_iff_mul_eq_right, cfcHom_eq_of_isStarNormal, CStarAlgebra.tendsto_mul_right_of_forall_nonneg_tendsto, 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, Unitary.path_apply, CStarAlgebra.nnnorm_mem_spectrum_of_nonneg, SpectrumRestricts.nnreal_iff_nnnorm, unitary.two_mul_one_sub_cos_norm_argSelfAdjoint, CStarAlgebra.le_nnnorm_of_mem_quasispectrum, CStarAlgebra.exists_sum_four_nonneg, PositiveLinearMap.preGNS_norm_sq, IsStarProjection.le_iff_idempotent_sub, 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, CStarAlgebra.norm_sub_mul_self_le_of_inr, Unitary.two_mul_one_sub_cos_norm_argSelfAdjoint
toNormedSpace 📖	CompOp	104 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.sqrt_inr, 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, Derivative.normalizedDerivOfComplex_mdifferentiable, 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, E2_mdifferentiable, WithCStarModule.prod_inner, summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp, Derivative.serreDerivative_mdifferentiable, 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	56 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, Unitization.sqrt_inr, 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, IsStarProjection.le_tfae, PositiveLinearMap.gnsStarAlgHom_apply, IsStarProjection.le_iff_sub, 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, CStarAlgebra.conjugate_le_norm_smul', CFC.nnrpow_le_nnrpow, CStarAlgebra.star_left_conjugate_le_norm_smul, Filter.IsIncreasingApproximateUnit.eventually_star_eq, CStarModule.inner_mul_inner_swap_le, CFC.monotone_sqrt, 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, CFC.sqrt_le_sqrt, CStarModule.continuous_inner, PositiveLinearMap.instStarHomClassOfLinearMapClassComplexOfOrderHomClass, CStarAlgebra.spectralOrderedRing, WithCStarModule.pi_norm_sq, CStarAlgebra.star_right_conjugate_le_norm_smul, 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	15 math math: summableLocallyUniformlyOn_iteratedDerivWithin_cexp, iteratedDerivWithin_tsum_cexp_eq, gelfandStarTransform_naturality, gelfandStarTransform_apply_apply, Unitization.sqrt_inr, gelfandStarTransform_symm_apply, cfcHom_real_eq_restrict, contDiffOn_tsum_cexp, cfcₙHom_real_eq_restrict, WStarAlgebra.exists_predual, Derivative.normalizedDerivOfComplex_mdifferentiable, E2_mdifferentiable, summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp, Derivative.serreDerivative_mdifferentiable, differentiableAt_iteratedDerivWithin_cexp
toNonUnitalNormedCommRing 📖	CompOp	73 math math: cfc_realPart, IsStarNormal.instNonUnitalContinuousFunctionalCalculus, Ideal.toCharacterSpace_apply_eq_zero_of_mem, cfc_im_id, CFC.monotoneOn_one_sub_one_add_inv, AlgHomClass.instStarHomClass, CFC.monotone_nnrpow, CFC.tendsto_cfc_rpow_sub_one_log, Unitization.real_cfcₙ_eq_cfc_inr, cfc_complex_eq_real, gelfandStarTransform_naturality, gelfandStarTransform_apply_apply, Unitization.sqrt_inr, ClosedSubmodule.inner_real_eq_re_inner, spectrum.gelfandTransform_eq, cfcₙ_re_id, gelfandStarTransform_symm_apply, CStarModule.inner_smul_left_complex, StarAlgebra.elemental.bijective_characterSpaceToSpectrum, gelfandTransform_map_star, cfcₙ_real_eq_complex, cfcₙ_comp_re, cfc_comp_im, IsSelfAdjoint.cfc_arg, cfcₙ_comp_im, cfcHom_real_eq_restrict, ClosedSubmodule.mem_symplComp_iff, CFC.log_monotoneOn, toCompleteSpace, CFC.monotone_rpow, inr_comp_cfcₙHom_eq_cfcₙAux, CFC.monotoneOn_one_sub_one_add_inv_real, instNonemptyElemWeakDualComplexCharacterSpaceOfNontrivial, cfcₙ_imaginaryPart, CFC.rpow_le_rpow, cfc_comp_re, toStarModule, selfAdjoint.star_coe_unitarySelfAddISMul, CStarAlgebra.rpow_neg_one_le_rpow_neg_one, cfcₙ_im_id, Unitization.nnreal_cfcₙ_eq_cfc_inr, toCStarRing, WStarAlgebra.exists_predual, CFC.nnrpow_le_nnrpow, IsStarNormal.instContinuousFunctionalCalculus, WeakDual.CharacterSpace.mem_spectrum_iff_exists, CStarAlgebra.rpow_neg_one_le_one, CFC.monotone_sqrt, norm_cfcₙ_one_sub_one_add_inv_lt_one, IsStarNormal.instNonUnitalIsometricContinuousFunctionalCalculus, Unitization.complex_cfcₙ_eq_cfc_inr, CFC.log_le_log, CFC.sqrt_le_sqrt, cfc_re_id, WeakDual.Complex.instStarHomClass, IsSelfAdjoint.self_add_I_smul_cfcSqrt_sub_sq_mem_unitary, toSMulCommClass, cfcₙ_realPart, cfc_real_eq_complex, StarAlgebra.elemental.continuous_characterSpaceToSpectrum, CFC.monotoneOn_cfcₙ_rpowIntegrand₀₁, IsStarNormal.instIsometricContinuousFunctionalCalculus, WeakDual.CharacterSpace.exists_apply_eq_zero, cfcHom_eq_of_isStarNormal, continuousFunctionalCalculus_map_id, CFC.conjugate_rpow_neg_one_half, CFC.complex_exp_eq_normedSpace_exp, le_iff_norm_sqrt_mul_rpow, cfcₙ_complex_eq_real, WeakDual.CharacterSpace.instStarHomClass, toIsScalarTower, le_iff_norm_sqrt_mul_sqrt_inv, cfc_imaginaryPart
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	144 math math: cfc_realPart, IsStarNormal.instNonUnitalContinuousFunctionalCalculus, IsSelfAdjoint.quasispectrumRestricts, Ideal.toCharacterSpace_apply_eq_zero_of_mem, EisensteinSeries.hasSum_e2Summand_symmetricIcc, cfc_im_id, CFC.monotoneOn_one_sub_one_add_inv, AlgHomClass.instStarHomClass, CFC.monotone_nnrpow, tsum_eisSummand_eq_riemannZeta_mul_eisensteinSeries, CFC.tendsto_cfc_rpow_sub_one_log, summableLocallyUniformlyOn_iteratedDerivWithin_cexp, Unitization.real_cfcₙ_eq_cfc_inr, StarAlgebra.elemental.characterSpaceToSpectrum_coe, iteratedDerivWithin_tsum_cexp_eq, CStarModule.innerSL_apply, cfc_complex_eq_real, ModularForm.discriminant_bounded_factor, gelfandStarTransform_naturality, gelfandStarTransform_apply_apply, ModularForm.tsum_logDeriv_eta_q, EisensteinSeries.summable_left_one_div_linear_sub_one_div_linear, CStarMatrix.toCLM_injective, Unitization.sqrt_inr, gelfandTransform_bijective, EisensteinSeries.e2Summand_summable, CStarMatrix.norm_def', ModularForm.discriminant_isZeroAtImInfty, CStarMatrix.inner_toCLM_conjTranspose_left, PositiveLinearMap.preGNS_norm_def, summable_eisSummand, CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM, ClosedSubmodule.inner_real_eq_re_inner, spectrum.gelfandTransform_eq, EisensteinSeries.tsum_symmetricIco_linear_sub_linear_add_one_eq_zero, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply_coe, cfcₙ_re_id, 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, cfcₙ_comp_re, VonNeumannAlgebra.coe_mk, cfc_comp_im, IsSelfAdjoint.cfc_arg, EisensteinSeries.hasSum_e2Summand_symmetricIco, EisensteinSeries.q_expansion_riemannZeta, cfcₙ_comp_im, VonNeumannAlgebra.mem_carrier, ModularForm.differentiableAt_eta_tprod, ModularForm.discriminant_eq_q_prod, ModularForm.logDeriv_one_sub_mul_cexp_comp, cfcHom_real_eq_restrict, ClosedSubmodule.mem_symplComp_iff, CStarMatrix.toCLM_apply_single, IsSelfAdjoint.spectrumRestricts, CFC.log_monotoneOn, CStarMatrix.toCLM_apply_eq_sum, CFC.monotone_rpow, inr_comp_cfcₙHom_eq_cfcₙAux, CFC.monotoneOn_one_sub_one_add_inv_real, CStarMatrix.toCLM_apply, ModularForm.logDeriv_eta_eq_E2, PositiveLinearMap.gnsStarAlgHom_apply, isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts, instNonemptyElemWeakDualComplexCharacterSpaceOfNontrivial, cfcₙ_imaginaryPart, CFC.rpow_le_rpow, ModularForm.differentiableAt_eta_of_mem_upperHalfPlaneSet, cfc_comp_re, CStarMatrix.mul_entry_mul_eq_inner_toCLM, ModularForm.logDeriv_one_sub_cexp, contDiffOn_tsum_cexp, EisensteinSeries.qExpansion_identity_pnat, selfAdjoint.star_coe_unitarySelfAddISMul, CStarAlgebra.rpow_neg_one_le_rpow_neg_one, cfcₙ_im_id, 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, CFC.nnrpow_le_nnrpow, EisensteinSeries.q_expansion_bernoulli, IsStarNormal.instContinuousFunctionalCalculus, SummableLocallyUniformlyOn.differentiableOn, EisensteinSeries.tendsto_double_sum_S_act, WeakDual.CharacterSpace.mem_spectrum_iff_exists, CStarAlgebra.rpow_neg_one_le_one, Derivative.normalizedDerivOfComplex_mdifferentiable, EisensteinSeries.summable_e2Summand_symmetricIcc, CFC.monotone_sqrt, norm_cfcₙ_one_sub_one_add_inv_lt_one, 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, CFC.log_le_log, CFC.sqrt_le_sqrt, cfc_re_id, EisensteinSeries.tendsto_tsum_one_div_linear_sub_succ_eq, WeakDual.Complex.instStarHomClass, IsSelfAdjoint.self_add_I_smul_cfcSqrt_sub_sq_mem_unitary, cfcₙ_realPart, 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, CFC.monotoneOn_cfcₙ_rpowIntegrand₀₁, IsStarNormal.instIsometricContinuousFunctionalCalculus, ModularForm.logDeriv_qParam, WeakDual.CharacterSpace.exists_apply_eq_zero, E2_mdifferentiable, cfcHom_eq_of_isStarNormal, summable_pow_mul_cexp, summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp, Derivative.serreDerivative_mdifferentiable, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply, continuousFunctionalCalculus_map_id, CFC.conjugate_rpow_neg_one_half, EisensteinSeries.tsum_symmetricIco_tsum_eq_S_act, CFC.complex_exp_eq_normedSpace_exp, le_iff_norm_sqrt_mul_rpow, cfcₙ_complex_eq_real, PositiveLinearMap.preGNS_norm_sq, WeakDual.CharacterSpace.instStarHomClass, CStarMatrix.norm_def, ModularForm.multipliableLocallyUniformlyOn_eta, differentiableAt_iteratedDerivWithin_cexp, CStarMatrix.inner_toCLM_conjTranspose_right, CStarMatrix.toCLM_apply_single_apply, le_iff_norm_sqrt_mul_sqrt_inv, cfc_imaginaryPart, 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