Basic

📁 Source: Mathlib/Analysis/Complex/Basic.lean

Statistics

Metric	Count
Definitions conjCLE, conjLIE, equivRealProdCLM, imCLM, instDenselyNormedField, instModuleSelf, instNormedAlgebraOfReal, instNormedField, instRCLike, ofRealCLM, ofRealLI, reCLM, slitPlane, complexToReal, complexToReal, complexLinearIsometryEquiv, complexRingEquiv	17
Theorems antilipschitz_equivRealProd, ball_one_subset_slitPlane, closedEmbedding_intCast, compl_Iic_zero, conjCLE_apply, conjCLE_coe, conjLIE_apply, conjLIE_symm, conj_mul', conj_tsum, continuous_conj, continuous_im, continuous_normSq, continuous_ofReal, continuous_re, dist_conj_comm, dist_conj_conj, eq_coe_norm_of_nonneg, equivRealProdCLM_apply, equivRealProdCLM_symm_apply, equivRealProdCLM_symm_apply_im, equivRealProdCLM_symm_apply_re, equivRealProd_apply_le, equivRealProd_apply_le', exists_norm_eq_mul_self, exists_norm_mul_eq_self, hasSum_conj, hasSum_conj', hasSum_iff, hasSum_im, hasSum_ofReal, hasSum_re, imCLM_apply, imCLM_coe, im_eq_zero_iff_isSelfAdjoint, im_tsum, instCompleteSpace, instContinuousStar, instProperSpace, instT2Space, inv_eq_conj, isClosed_range_intCast, isOpen_compl_range_intCast, isOpen_slitPlane, isUniformEmbedding_equivRealProd, isUniformEmbedding_ofReal, isometry_conj, isometry_intCast, isometry_ofReal, le_of_eq_sum_of_eq_sum_norm, lipschitz_equivRealProd, mem_slitPlane_iff, mem_slitPlane_iff_not_le_zero, mem_slitPlane_of_norm_lt_one, mem_slitPlane_or_neg_mem_slitPlane, mul_conj', natCast_mem_slitPlane, neg_ofReal_mem_slitPlane, nndist_conj_comm, nndist_conj_conj, nnnorm_eq_one_of_pow_eq_one, nnnorm_intCast, norm_eq_one_of_pow_eq_one, norm_of_nonneg', ofNat_mem_slitPlane, ofRealCLM_apply, ofRealCLM_coe, ofRealLI_apply, ofReal_eq_re_of_isSelfAdjoint, ofReal_mem_slitPlane, ofReal_tsum, one_mem_slitPlane, orderClosedTopology, reCLM_apply, reCLM_coe, re_eq_ofReal_of_isSelfAdjoint, re_le_re, re_nonneg_iff_nonneg, re_tsum, restrictScalars_one_smulRight, restrictScalars_one_smulRight', restrictScalars_toSpanSingleton, restrictScalars_toSpanSingleton', ringHom_eq_id_or_conj_of_continuous, ringHom_eq_ofReal_of_continuous, slitPlane_eq_union, slitPlane_ne_zero, subset_slitPlane_iff_of_subset_sphere, summable_conj, summable_ofReal, tendsto_normSq_cocompact_atTop, uniformContinuous_im, uniformContinuous_re, uniformlyContinuous_im, uniformlyContinuous_re, zero_notMem_slitPlane, ofReal, tendsto_ofReal_iff, tendsto_ofReal_iff', reProdIm, I_to_complex, complexLinearIsometryEquiv_apply, complexLinearIsometryEquiv_symm_apply, complexRingEquiv_apply, complexRingEquiv_symm_apply, conj_tsum, hasSum_conj, hasSum_conj', hasSum_iff, hasSum_im, hasSum_ofReal, hasSum_re, im_eq_complex_im, im_to_complex, im_tsum, isUniformEmbedding_ofReal, map_nonneg_iff, normSq_to_complex, norm_to_complex, ofReal_eq_complex_ofReal, ofReal_tsum, re_eq_complex_re, re_to_complex, re_tsum, summable_conj, summable_ofReal, toContinuousLinearMap_complexLinearIsometryEquiv, to_complex_nonneg_iff, norm_le, norm_le	130
Total	147

Complex

Definitions

Name	Category	Theorems
conjCLE 📖	CompOp	8 math math: IsConformalMap.is_complex_or_conj_linear, conjCLE_nnorm, isConformalMap_complex_linear_conj, conjCLE_enorm, conjCLE_apply, conjCLE_norm, isConformalMap_iff_is_complex_or_conj_linear, conjCLE_coe
conjLIE 📖	CompOp	7 math math: isConformalMap_conj, linearEquiv_det_conjLIE, conjLIE_apply, linear_isometry_complex, linear_isometry_complex_aux, det_conjLIE, conjLIE_symm
equivRealProdCLM 📖	CompOp	4 math math: equivRealProdCLM_symm_apply, equivRealProdCLM_symm_apply_re, equivRealProdCLM_symm_apply_im, equivRealProdCLM_apply
imCLM 📖	CompOp	10 math math: restrictScalars_one_smulRight', HasDerivWithinAt.complexToReal_fderiv', imCLM_norm, HasDerivAt.complexToReal_fderiv', HasStrictDerivAt.complexToReal_fderiv', imCLM_coe, imCLM_nnnorm, imCLM_enorm, imCLM_apply, restrictScalars_toSpanSingleton'
instDenselyNormedField 📖	CompOp	338 math math: WeakFEPair.differentiableAt_Λ, UpperHalfPlane.mdifferentiable_num, HurwitzZeta.differentiableAt_hurwitzZetaEven_sub_one_div, ZMod.differentiableAt_LFunction, differentiableAt_sin, differentiable_const_cpow_of_neZero, CuspFormClass.holo, HurwitzZeta.differentiableAt_hurwitzZeta_sub_one_div, ModularFormClass.differentiableAt_comp_ofComplex, PeriodPair.hasFPowerSeriesAt_weierstrassPExcept, HurwitzZeta.differentiableAt_hurwitzZetaEven, ModularFormClass.qExpansionFormalMultilinearSeries_apply_norm, ModularFormClass.hasFPowerSeries_cuspFunction, iteratedDeriv_even_cosh, ModularFormClass.qExpansionFormalMultilinearSeries_radius, PeriodPair.deriv_weierstrassP, PeriodPair.coeff_weierstrassPExceptSeries, complexOfReal_hasDerivWithinAt, analyticAt_cosh, meromorphic_digamma, PeriodPair.iteratedDeriv_weierstrassPExcept_self, norm_jacobiTheta₂_term_fderiv_ge, summableLocallyUniformlyOn_iteratedDerivWithin_cexp, one_add_cpow_hasFPowerSeriesAt_zero, DirichletCharacter.continuousOn_neg_logDeriv_LFunction_of_nontriv, Unitization.real_cfcₙ_eq_cfc_inr, analyticOn_sin, HasFDerivWithinAt.complexOfReal, ProbabilityTheory.hasDerivAt_integral_pow_mul_exp, iteratedDeriv_odd_sinh, hasStrictDerivAt_tan, iteratedDerivWithin_tsum_cexp_eq, PeriodPair.iteratedDeriv_derivWeierstrassPExcept_self, PeriodPair.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept, DirichletCharacter.LSeries_twist_vonMangoldt_eq, deriv_cos, not_differentiableAt_Gamma_neg_nat, differentiableOn_dslope, differentiableOn_iteratedDerivWithin_cotTerm, differentiableAt_GammaAux, gelfandStarTransform_naturality, HarmonicAt.analyticAt_complex_partial, PeriodPair.analyticAt_weierstrassPExcept, summableLocallyUniformlyOn_iteratedDerivWithin_cotTerm, analyticWithinAt_cosh, DirichletCharacter.deriv_LFunction_eq_deriv_LSeries, ModularForm.tsum_logDeriv_eta_q, StrongFEPair.differentiable_Λ, ZMod.differentiableAt_completedLFunction, contDiff_cosh, analyticOn_cosh, hasDerivAt_GammaIntegral, LSeries_iteratedDeriv, analyticOnNhd_univ_iff_differentiable, CStarMatrix.norm_def', analyticOn_sinh, UpperHalfPlane.mdifferentiable_inv_denom, hasStrictFDerivAt_cpow', HurwitzZeta.differentiable_expZeta_of_ne_zero, mellin_hasDerivAt_of_isBigO_rpow, HurwitzZeta.differentiable_hurwitzZetaOdd, LSeries_deriv_eqOn, HurwitzZeta.differentiable_hurwitzZeta_sub_hurwitzZeta, PeriodPair.hasFPowerSeriesAt_derivWeierstrassPExcept, LSeries_analyticOnNhd, deriv_Gamma_add_one, UpperHalfPlane.contMDiff_coe, CuspForm.holo', analyticAt_sin, PeriodPair.analyticOnNhd_derivWeierstrassPExcept, iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow, DirichletCharacter.differentiableAt_LFunction, hasDerivAt_Gammaℝ_one, hasFDerivAt_jacobiTheta₂_term, LSeries_deriv, UpperHalfPlane.contMDiff_inv_denom, norm_cauchyPowerSeries_le, ProbabilityTheory.iteratedDeriv_complexMGF, contDiffAt_log, hasStrictFDerivAt_cpow, differentiable_iteratedDeriv_sin, hasStrictDerivAt_sinh, Real.fourier_mul_convolution_eq, iteratedDeriv_odd_sin, HarmonicAt.differentiableAt_complex_partial, tendsto_logDeriv_euler_sin_div, EisensteinSeries.div_linear_zpow_differentiableOn, ZMod.differentiable_completedLFunction, logDeriv_sin_div_eq_cot, logDeriv_sin, ProbabilityTheory.analyticAt_complexMGF, deriv_Gamma_nat, PeriodPair.weierstrassPExcept_eq_tsum, logDeriv_exp, IsExactOn.differentiableOn, hasDerivAt_jacobiTheta₂_fst, ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div, PeriodPair.differentiableOn_derivWeierstrassP, hasDerivAt_sinh, PeriodPair.meromorphic_derivWeierstrassP, SchwartzMap.convolution_apply, hasDerivAt_Gammaℂ_one, analyticOnNhd_sin, hasStrictDerivAt_const_cpow, one_add_cpow_hasFPowerSeriesAt_zero, UpperHalfPlane.contMDiff_num, UpperHalfPlane.mdifferentiable_denom, hasFDerivAt_cpow, differentiable_Gammaℝ_inv, differentiableAt_jacobiTheta₂_fst, iter_deriv_exp, differentiableAt_tan, ModularForm.differentiableAt_eta_tprod, eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet, one_div_sub_sq_hasFPowerSeriesOnBall_zero, hasDerivAt_cos, differentiableAt_complex_iff_differentiableAt_real, eqOn_iteratedDeriv_cotTerm, one_div_one_sub_pow_hasFPowerSeriesOnBall_zero, hasStrictDerivAt_log, analyticOnNhd_cexp, ProbabilityTheory.hasDerivAt_complexMGF, ModularFormClass.qExpansion_coeff, HurwitzZeta.differentiableAt_completedHurwitzZetaEven, HurwitzZeta.differentiableAt_one_completedHurwitzZetaEven_sub_completedHurwitzZetaEven, complexOfReal_deriv, le_radius_cauchyPowerSeries, analyticOn_iff_differentiableOn, differentiable_sin, ModularForm.logDeriv_eta_eq_E2, PeriodPair.order_weierstrassP, analyticOn_cos, differentiableOn_compl_singleton_and_continuousAt_iff, MeromorphicNFOn.Gamma, hasDerivAt_logTaylor, DirichletCharacter.differentiable_LFunction, iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow, iteratedDeriv_add_one_sinh, iteratedDeriv_even_cos, ModularForm.differentiableAt_eta_of_mem_upperHalfPlaneSet, complexOfReal_fderivWithin, iteratedDeriv_add_one_sin, Real.fourier_bilin_convolution_eq, one_div_sub_pow_hasFPowerSeriesOnBall_zero, ModularFormClass.differentiableAt_cuspFunction, ModularForm.logDeriv_one_sub_cexp, HadamardThreeLines.diffContOnCl_interpStrip, hasFPowerSeriesOn_cauchy_integral, UpperHalfPlane.contMDiff_denom_zpow, contDiffOn_tsum_cexp, ValueDistribution.logCounting_congr_codiscrete, analyticAt_sinh, hasStrictDerivAt_cos, analyticOn_univ_iff_differentiable, iteratedDeriv_add_one_cos, ArithmeticFunction.LSeries_vonMangoldt_eq, DirichletCharacter.differentiableAt_completedLFunction, cot_pi_mul_contDiffWithinAt, digamma_def, HasFDerivAt.complexOfReal_hasFDerivAt, PeriodPair.coeff_weierstrassPSeries, deriv_cosh, locallyFinsuppWithin.logCounting_divisor, hasStrictDerivAt_sin, contDiffAt_tan, analyticWithinAt_sinh, analyticOnNhd_cosh, hasFDerivAt_jacobiTheta₂, deriv_tan, hasDerivAt_cosh, Unitization.nnreal_cfcₙ_eq_cfc_inr, HurwitzZeta.differentiableAt_hurwitzZeta, contDiff_sinh, DirichletCharacter.deriv_LFunctionTrivChar₁_apply_of_ne_one, LSeries_differentiableOn, differentiableAt_riemannZeta, PeriodPair.hasFPowerSeriesOnBall_weierstrassP, harmonic_is_realOfHolomorphic, ModularForm.summable_logDeriv_one_sub_eta_q, PeriodPair.weierstrassPSeries_hasSum, hasDerivAt_sin, analyticOn_cexp, WStarAlgebra.exists_predual, LSeries.iteratedDeriv_alternating, PeriodPair.deriv_derivWeierstrassPExcept_self, hasStrictDerivAt_exp, hasStrictDerivAt_cosh, isConservativeOn_and_continuousOn_iff_isDifferentiableOn, PeriodPair.hasFPowerSeriesOnBall_derivWeierstrassPExcept, differentiableAt_const_cpow_of_neZero, LogDeriv_exp, differentiable_one_div_Gamma, not_differentiableAt_Gamma_zero, ProbabilityTheory.differentiableOn_complexMGF, PeriodPair.deriv_weierstrassPExcept_same, PeriodPair.analyticOnNhd_derivWeierstrassP, hasFPowerSeriesOnBall_cuspFunction, one_div_one_sub_cpow_hasFPowerSeriesOnBall_zero, HurwitzZeta.differentiableAt_completedCosZeta, ArithmeticFunction.vonMangoldt.LSeries_residueClass_eq, PeriodPair.meromorphic_weierstrassP, PeriodPair.analyticAt_derivWeierstrassPExcept, differentiableAt_cosh, differentiableAt_Gamma_nat_add_one, deriv_cos', differentiableAt_jacobiTheta₂_snd, one_add_cpow_hasFPowerSeriesOnBall_zero, SchwartzMap.fderivCLM_fourier_eq, hasStrictDerivAt_cpow_const, mellin_differentiableAt_of_isBigO_rpow_exp, LSeries_analyticOn, iteratedDeriv_odd_cos, one_div_one_sub_sq_hasFPowerSeriesOnBall_zero, HurwitzZeta.differentiable_cosZeta_of_ne_zero, deriv_cpow_const, IsConservativeOn.hasDerivAt_wedgeIntegral, logDeriv_prod_sineTerm_eq_sum_cotTerm, differentiableAt_Gamma_one, mdifferentiable_jacobiTheta, PeriodPair.hasFPowerSeriesOnBall_weierstrassPExcept, hasDerivAt_Gamma_one, ProbabilityTheory.hasDerivAt_iteratedDeriv_complexMGF, iteratedDeriv_even_sin, UpperHalfPlane.contMDiffAt_ofComplex, Unitization.complex_cfcₙ_eq_cfc_inr, ModularForm.holo', ProbabilityTheory.analyticOn_complexMGF, differentiable_completedZeta₀, differentiable_sinh, iteratedDeriv_even_sinh, iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum, differentiable_iteratedDeriv_sinh, UpperHalfPlane.contMDiffAt_iff, UpperHalfPlane.instIsManifoldComplexModelWithCornersSelfTopWithTopENat, differentiableAt_sinh, hasDerivAt_Gamma_one_half, Function.Periodic.differentiable_qParam, Function.Periodic.contDiff_qParam, PeriodPair.differentiableOn_weierstrassPExcept, analyticOnNhd_iff_differentiableOn, differentiableAt_log, differentiableAt_completedZeta, iteratedDeriv_add_one_cosh, PeriodPair.differentiableOn_weierstrassP, UpperHalfPlane.mdifferentiable_coe, complexOfReal_fderiv, PeriodPair.weierstrassPExceptSeries_hasSum, EisensteinSeries.eisSummand_extension_differentiableOn, ModularFormClass.analyticAt_cuspFunction_zero, deriv_sinh, HadamardThreeLines.diffContOnCl_invInterpStrip, deriv_sin, hasDerivAt_tan, analyticWithinAt_sin, conformalAt_iff_differentiableAt_or_differentiableAt_comp_conj, analyticAt_clog, complexOfReal_hasDerivAt, ModularFormClass.differentiableOn_cuspFunction_ball, ZMod.differentiable_completedLFunction₀, ModularFormClass.holo, iteratedDeriv_cexp_const_mul, SchwartzMap.fourier_fderivCLM_eq, SchwartzMap.fourier_convolution_apply, differentiableAt_Gamma, HurwitzZeta.differentiableAt_cosZeta, logDeriv_cos, gelfandTransform_isometry, mellin_differentiableAt_of_isBigO_rpow, one_add_cpow_hasFPowerSeriesOnBall_zero, differentiable_cosh, EisensteinSeries.eisensteinSeries_SIF_MDifferentiable, differentiable_iteratedDeriv_cos, differentiable_cos, LSeries_hasDerivAt, one_div_one_sub_hasFPowerSeriesOnBall_zero, UpperHalfPlane.mdifferentiableAt_iff, PeriodPair.analyticOnNhd_weierstrassPExcept, analyticAt_cos, analyticOnNhd_cos, ArithmeticFunction.iteratedDeriv_LSeries_alternating, analyticWithinAt_cexp, iteratedDeriv_odd_cosh, differentiableWithinAt_complex_iff_differentiableWithinAt_real, contDiff_sin, hasDerivAt_exp, contDiff_cos, Meromorphic.Gamma, hasDerivAt_log_sub_logTaylor, ProbabilityTheory.analyticOnNhd_complexMGF, ModularForm.logDeriv_qParam, hasDerivAt_log, ModularFormClass.qExpansionFormalMultilinearSeries_coeff, UpperHalfPlane.contMDiff_smul, eqOn_iteratedDerivWithin_cotTerm_integerComplement, UpperHalfPlane.contMDiff_denom, logDeriv_sineTerm_eq_cotTerm, one_div_sub_sq_sub_one_div_sq_hasFPowerSeriesOnBall_zero, ZMod.differentiable_LFunction_of_sum_zero, EisensteinSeries.eisensteinSeriesSIF_mdifferentiable, PeriodPair.analyticOnNhd_weierstrassP, differentiableAt_cos, UpperHalfPlane.mdifferentiable_denom_zpow, MeromorphicOn.Gamma, complexOfReal_derivWithin, hasFPowerSeriesOnBall_ofScalars_mul_add_zero, HurwitzZeta.differentiable_completedHurwitzZetaEven₀, HurwitzZeta.differentiable_completedHurwitzZetaOdd, summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp, deriv_exp, DirichletCharacter.differentiable_LFunctionTrivChar₁, UpperHalfPlane.mdifferentiable_iff, analyticAt_iff_eventually_differentiableAt, HurwitzZeta.differentiable_completedSinZeta, HurwitzZeta.differentiable_hurwitzZetaEven_sub_hurwitzZetaEven, analyticOnNhd_sinh, analyticWithinAt_cos, LSeries.hasDerivAt_term, UpperHalfPlane.mdifferentiableAt_ofComplex, Real.fourier_smul_convolution_eq, WeakFEPair.differentiable_Λ₀, DirichletCharacter.continuousOn_neg_logDeriv_LFunctionTrivChar₁, DirichletCharacter.differentiable_completedLFunction, HurwitzZeta.differentiableAt_expZeta, logDeriv_cosh, one_div_sub_hasFPowerSeriesOnBall_zero, CStarMatrix.norm_def, HurwitzZeta.differentiableAt_sinZeta, TemperedDistribution.smulLeftCLM_apply_apply, differentiableAt_jacobiTheta, differentiableAt_iteratedDerivWithin_cexp, hasDerivAt_Gamma_nat, norm_jacobiTheta₂_term_fderiv_le, UpperHalfPlane.mdifferentiable_smul, Unitization.cfcₙ_eq_cfc_inr, HurwitzZeta.differentiable_completedCosZeta₀, differentiable_iteratedDeriv_cosh, analyticAt_cexp, PeriodPair.differentiableOn_derivWeierstrassPExcept
instModuleSelf 📖	CompOp	217 math math: WeakFEPair.differentiableAt_Λ, HurwitzZeta.differentiableAt_hurwitzZetaEven_sub_one_div, ZMod.differentiableAt_LFunction, differentiableAt_sin, differentiable_const_cpow_of_neZero, HurwitzZeta.differentiableAt_hurwitzZeta_sub_one_div, ModularFormClass.differentiableAt_comp_ofComplex, HurwitzZeta.differentiableAt_hurwitzZetaEven, ModularFormClass.qExpansionFormalMultilinearSeries_apply_norm, NumberField.canonicalEmbedding.mem_span_latticeBasis, PeriodPair.deriv_weierstrassP, complexOfReal_hasDerivWithinAt, norm_jacobiTheta₂_term_fderiv_ge, NumberField.canonicalEmbedding.latticeBasis_apply, span_fourier_closure_eq_top, ZMod.LFunction_one_sub, DirichletCharacter.continuousOn_neg_logDeriv_LFunction_of_nontriv, ZMod.dft_even_iff, Unitization.real_cfcₙ_eq_cfc_inr, HasFDerivWithinAt.complexOfReal, ProbabilityTheory.hasDerivAt_integral_pow_mul_exp, IsConformalMap.is_complex_or_conj_linear, hasStrictDerivAt_tan, UnitAddTorus.mFourierSubalgebra_coe, PeriodPair.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept, sum_cauchyPowerSeries_eq_integral, DirichletCharacter.LSeries_twist_vonMangoldt_eq, deriv_cos, not_differentiableAt_Gamma_neg_nat, differentiableOn_dslope, differentiableOn_iteratedDerivWithin_cotTerm, differentiableAt_GammaAux, DirichletCharacter.deriv_LFunction_eq_deriv_LSeries, StrongFEPair.differentiable_Λ, ZMod.differentiableAt_completedLFunction, hasDerivAt_GammaIntegral, analyticOnNhd_univ_iff_differentiable, TemperedDistribution.instLineDerivLeftSMulReal, hasStrictFDerivAt_cpow', PositiveLinearMap.preGNS_norm_def, UnitAddTorus.mFourierCoeff_toLp, HurwitzZeta.differentiable_expZeta_of_ne_zero, HurwitzZeta.differentiable_hurwitzZetaOdd, LSeries_deriv_eqOn, HurwitzZeta.differentiable_hurwitzZeta_sub_hurwitzZeta, cauchyPowerSeries_apply, deriv_Gamma_add_one, DirichletCharacter.differentiableAt_LFunction, NumberField.canonicalEmbedding.integralBasis_repr_apply, hasDerivAt_Gammaℝ_one, hasFDerivAt_jacobiTheta₂_term, LSeries_deriv, gelfandStarTransform_symm_apply, norm_cauchyPowerSeries_le, summable_jacobiTheta₂_term_fderiv_iff, hasSum_fourier_series_L2, hasStrictFDerivAt_cpow, differentiable_iteratedDeriv_sin, hasStrictDerivAt_sinh, PositiveLinearMap.preGNS_inner_def, HarmonicAt.differentiableAt_complex_partial, EisensteinSeries.div_linear_zpow_differentiableOn, ZMod.differentiable_completedLFunction, deriv_Gamma_nat, IsExactOn.differentiableOn, hasDerivAt_jacobiTheta₂_fst, ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div, PeriodPair.differentiableOn_derivWeierstrassP, hasDerivAt_sinh, hasSum_jacobiTheta₂_term_fderiv, hasDerivAt_Gammaℂ_one, hasStrictDerivAt_const_cpow, hasSum_cauchyPowerSeries_integral, LinearMap.coe_complexOfReal, hasFDerivAt_cpow, differentiable_Gammaℝ_inv, differentiableAt_jacobiTheta₂_fst, iter_deriv_exp, differentiableAt_tan, ModularForm.differentiableAt_eta_tprod, hasDerivAt_cos, differentiableAt_complex_iff_differentiableAt_real, cfcHom_real_eq_restrict, restrictScalars_one_smulRight, hasStrictDerivAt_log, fourierCoeff_toLp, ProbabilityTheory.hasDerivAt_complexMGF, HurwitzZeta.differentiableAt_completedHurwitzZetaEven, HurwitzZeta.differentiableAt_one_completedHurwitzZetaEven_sub_completedHurwitzZetaEven, TemperedDistribution.instLineDerivSMulReal, analyticOn_iff_differentiableOn, differentiable_sin, differentiableOn_compl_singleton_and_continuousAt_iff, hasDerivAt_logTaylor, DirichletCharacter.differentiable_LFunction, UnitAddTorus.instContinuousSMulComplexSubtypeAEEqFunVolumeMemAddSubgroupLp, UnitAddTorus.hasSum_mFourier_series_L2, ModularForm.differentiableAt_eta_of_mem_upperHalfPlaneSet, complexOfReal_fderivWithin, ModularFormClass.differentiableAt_cuspFunction, QuadraticForm.equivalent_sum_squares, hasStrictDerivAt_cos, analyticOn_univ_iff_differentiable, ArithmeticFunction.LSeries_vonMangoldt_eq, DirichletCharacter.IsPrimitive.fourierTransform_eq_inv_mul_gaussSum, DirichletCharacter.differentiableAt_completedLFunction, HasFDerivAt.complexOfReal_hasFDerivAt, restrictScalars_toSpanSingleton, deriv_cosh, fourierSubalgebra_coe, hasStrictDerivAt_sin, hasFDerivAt_jacobiTheta₂, deriv_tan, hasDerivAt_cosh, Unitization.nnreal_cfcₙ_eq_cfc_inr, HurwitzZeta.differentiableAt_hurwitzZeta, DirichletCharacter.deriv_LFunctionTrivChar₁_apply_of_ne_one, isConformalMap_complex_linear_conj, LSeries_differentiableOn, differentiableAt_riemannZeta, cfcₙHom_real_eq_restrict, NumberField.canonicalEmbedding.mem_rat_span_latticeBasis, hasDerivAt_sin, WStarAlgebra.exists_predual, span_fourierLp_closure_eq_top, PeriodPair.deriv_derivWeierstrassPExcept_self, hasStrictDerivAt_exp, hasStrictDerivAt_cosh, isConservativeOn_and_continuousOn_iff_isDifferentiableOn, differentiableAt_const_cpow_of_neZero, differentiable_one_div_Gamma, ZMod.completedLFunction_one_sub_odd, not_differentiableAt_Gamma_zero, ProbabilityTheory.differentiableOn_complexMGF, PeriodPair.deriv_weierstrassPExcept_same, HurwitzZeta.differentiableAt_completedCosZeta, ArithmeticFunction.vonMangoldt.LSeries_residueClass_eq, differentiableAt_cosh, differentiableAt_Gamma_nat_add_one, deriv_cos', differentiableAt_jacobiTheta₂_snd, hasStrictDerivAt_cpow_const, mellin_differentiableAt_of_isBigO_rpow_exp, HurwitzZeta.differentiable_cosZeta_of_ne_zero, deriv_cpow_const, differentiableAt_Gamma_one, hasDerivAt_Gamma_one, ProbabilityTheory.hasDerivAt_iteratedDeriv_complexMGF, differentiable_completedZeta₀, differentiable_sinh, differentiable_iteratedDeriv_sinh, differentiableAt_sinh, hasDerivAt_Gamma_one_half, Function.Periodic.differentiable_qParam, PeriodPair.differentiableOn_weierstrassPExcept, analyticOnNhd_iff_differentiableOn, differentiableAt_log, differentiableAt_completedZeta, PeriodPair.differentiableOn_weierstrassP, UnitAddTorus.span_mFourier_closure_eq_top, complexOfReal_fderiv, EisensteinSeries.eisSummand_extension_differentiableOn, deriv_sinh, deriv_sin, hasDerivAt_tan, conformalAt_iff_differentiableAt_or_differentiableAt_comp_conj, complexOfReal_hasDerivAt, ModularFormClass.differentiableOn_cuspFunction_ball, ZMod.differentiable_completedLFunction₀, differentiableAt_Gamma, HurwitzZeta.differentiableAt_cosZeta, jacobiTheta₂_fderiv_undef, mellin_differentiableAt_of_isBigO_rpow, differentiable_cosh, ContinuousLinearMap.coe_complexOfReal, ZMod.completedLFunction_one_sub_even, differentiable_iteratedDeriv_cos, AddChar.coe_complexBasis, differentiable_cos, LSeries_hasDerivAt, UpperHalfPlane.mdifferentiableAt_iff, isConformalMap_complex_linear, differentiableWithinAt_complex_iff_differentiableWithinAt_real, hasDerivAt_exp, DirichletCharacter.fourierTransform_eq_gaussSum_mulShift, NumberField.mixedEmbedding.disjoint_span_commMap_ker, hasDerivAt_log_sub_logTaylor, ZMod.dft_odd_iff, AddChar.complexBasis_apply, hasDerivAt_log, ZMod.differentiable_LFunction_of_sum_zero, UnitAddTorus.span_mFourierLp_closure_eq_top, ZMod.LFunction_dft, differentiableAt_cos, HurwitzZeta.differentiable_completedHurwitzZetaEven₀, HurwitzZeta.differentiable_completedHurwitzZetaOdd, deriv_exp, isConformalMap_iff_is_complex_or_conj_linear, DirichletCharacter.differentiable_LFunctionTrivChar₁, UpperHalfPlane.mdifferentiable_iff, analyticAt_iff_eventually_differentiableAt, HurwitzZeta.differentiable_completedSinZeta, HurwitzZeta.differentiable_hurwitzZetaEven_sub_hurwitzZetaEven, LSeries.hasDerivAt_term, WeakFEPair.differentiable_Λ₀, DirichletCharacter.continuousOn_neg_logDeriv_LFunctionTrivChar₁, DirichletCharacter.differentiable_completedLFunction, PositiveLinearMap.preGNS_norm_sq, HurwitzZeta.differentiableAt_expZeta, HurwitzZeta.differentiableAt_sinZeta, differentiableAt_jacobiTheta, differentiableAt_iteratedDerivWithin_cexp, hasDerivAt_Gamma_nat, norm_jacobiTheta₂_term_fderiv_le, HurwitzZeta.differentiable_completedCosZeta₀, differentiable_iteratedDeriv_cosh, PeriodPair.differentiableOn_derivWeierstrassPExcept
instNormedAlgebraOfReal 📖	CompOp	2 math math: restrictScalars_one_smulRight, restrictScalars_toSpanSingleton
instNormedField 📖	CompOp	1494 math math: ArithmeticFunction.vonMangoldt.residueClass_eq, HurwitzZeta.hasSum_int_hurwitzZetaOdd, NumberField.mixedEmbedding.integral_comp_polarSpaceCoord_symm, Real.hasDerivAt_fourier, WeakFEPair.differentiableAt_Λ, NumberField.basisMatrix_eq_embeddingsMatrixReindex, TemperedDistribution.lineDerivOpCLM_eq, NumberField.mixedEmbedding.fundamentalDomain_integerLattice, MeasureTheory.Lp.toTemperedDistributionCLM_apply, UpperHalfPlane.mdifferentiable_num, TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq, cos_eq_tsum, isConformalMap_conj, NumberField.InfinitePlace.Completion.isometry_extensionEmbeddingOfIsReal, ProbabilityTheory.integrable_cexp_mul_of_re_mem_integrableExpSet, NumberField.InfinitePlace.isNontrivial, HurwitzZeta.differentiableAt_hurwitzZetaEven_sub_one_div, NumberField.InfinitePlace.eq_iff_isEquiv, continuousAt_const_cpow, unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le, differentiableAt_sin, tendsto_log_nhdsWithin_im_neg_of_re_neg_of_im_zero, norm_circleTransformBoundingFunction_le, isOpen_re_lt_EReal, differentiable_const_cpow_of_neZero, NumberField.mixedEmbedding.normAtComplexPlaces_mixedSpaceOfRealSpace, IsStarNormal.instNonUnitalContinuousFunctionalCalculus, restrictScalars_one_smulRight', completedZeta_eq_tsum_of_one_lt_re, continuousOn_exp, IsSelfAdjoint.quasispectrumRestricts, CuspFormClass.holo, IsStarNormal.spectralRadius_eq_nnnorm, NumberField.mixedEmbedding.lintegral_comp_polarCoord_symm, SchwartzMap.integral_sesq_fourier_fourier, HurwitzZeta.differentiableAt_hurwitzZeta_sub_one_div, GaussianFourier.integrable_cexp_neg_mul_sq_add_real_mul_I, ModularFormClass.differentiableAt_comp_ofComplex, PeriodPair.hasFPowerSeriesAt_weierstrassPExcept, Real.hasFDerivAt_fourierChar_neg_bilinear_left, linearEquiv_det_conjLIE, Ideal.toCharacterSpace_apply_eq_zero_of_mem, Unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le, HurwitzZeta.differentiableAt_hurwitzZetaEven, ModularFormClass.qExpansionFormalMultilinearSeries_apply_norm, CFC.monotoneOn_one_sub_one_add_inv, NumberField.canonicalEmbedding.mem_span_latticeBasis, Real.fderiv_fourierIntegral, PeriodPair.hasSumLocallyUniformly_weierstrassP, NumberField.mixedEmbedding.norm_eq_sup'_normAtPlace, NonUnitalCStarAlgebra.toStarModule, circleTransformDeriv_eq, LSeries.term_sum, HurwitzZeta.hasSum_int_cosKernel₀, isOpenMap_im, HurwitzZeta.hasSum_int_hurwitzZetaEven, ofRealCLM_coe, kahler, norm_polarCoord_symm, finrank_real_complex_fact', PeriodPair.deriv_weierstrassP, PeriodPair.coeff_weierstrassPExceptSeries, Real.fourierIntegralInv_eq', PositiveLinearMap.apply_le_of_isSelfAdjoint, comap_exp_cobounded, ModularForm.mul_slash, Circle.exp_arg, Circle.injective_arg, CFC.monotone_nnrpow, DirichletCharacter.LSeries_eulerProduct_tprod, LSeries.term_convolution', ofRealLI_apply, CuspFormClass.zero_at_infty_comp_ofComplex, PeriodPair.derivWeierstrassPExcept_sub, norm_jacobiTheta₂_term_fderiv_ge, NumberField.canonicalEmbedding.latticeBasis_apply, integral_comp_pi_polarCoord_symm, CFC.tendsto_cfc_rpow_sub_one_log, HurwitzZeta.cosZeta_two_mul_nat', UpperHalfPlane.image_coe_sphere, isCoveringMap_exp, PeriodPair.ω₁_div_two_notMem_lattice, range_circleMap, continuousWithinAt_arg_of_re_neg_of_im_zero, span_fourier_closure_eq_top, Real.fourierIntegral_eq, GammaSeq_tendsto_Gamma, PeriodPair.basis_one, Orientation.kahler_comp_rightAngleRotation', circleIntegral_def_Icc, NumberField.isInfinitePlace_iff, one_add_cpow_hasFPowerSeriesAt_zero, circleIntegrable_iff, DirichletCharacter.continuousOn_neg_logDeriv_LFunction_of_nontriv, tsum_exp_neg_mul_int_sq, not_integrableOn_Ioi_cpow, Real.fderiv_fourierChar_neg_bilinear_right_apply, NumberField.InfinitePlace.isometry_embedding, BoundedContinuousFunction.char_neg, UpperHalfPlane.isOpenEmbedding_coe, Real.fourier_continuousLinearMap_apply, Unitization.real_cfcₙ_eq_cfc_inr, uniformlyContinuous_im, NumberField.mem_maximalRealSubfield_iff, BoundedContinuousFunction.char_zero_eq_one, SchwartzMap.lineDerivOp_fourier_eq, SchwartzMap.integral_bilin_fourierInv_eq, Function.Periodic.cuspFunction_zero_eq_limUnder_nhds_ne, UpperHalfPlane.comp_ofComplex_of_im_pos, NumberField.mixedEmbedding.normAtPlace_polarCoord_symm_of_isComplex, continuousOn_arg, lipschitz_equivRealProd, UpperHalfPlane.dist_le_iff_dist_coe_center_le, hasSum_one_div_nat_pow_mul_fourier, two_mul_riemannZeta_eq_tsum_int_inv_pow_of_even, NumberField.mixedEmbedding.norm_le_convexBodySumFun, UnitDisc.instSMulCommClass_closedBall_circle, TemperedDistribution.lineDerivOp_fourier_eq, frontier_setOf_re_le, WeakFEPair.symm_Λ₀_eq, VonNeumannAlgebra.ext_iff, ofRealCLM_norm, UnitDisc.instSMulCommClass_closedBall_left, ProbabilityTheory.hasDerivAt_integral_pow_mul_exp, StarAlgebra.elemental.characterSpaceToSpectrum_coe, HurwitzZeta.cosZeta_two_mul_nat, rotation_injective, Bornology.IsBounded.reProdIm, Circle.ofConjDivSelf_coe, NumberField.mixedEmbedding.mem_idealLattice, borelSpace, ProbabilityTheory.integrable_rpow_mul_cexp_of_re_mem_interior_integrableExpSet, convexHull_reProdIm, conjLIE_apply, hasStrictDerivAt_tan, Circle.starRingEnd_addChar, closure_preimage_im, NumberField.InfiniteAdeleRing.algebraMap_apply, UnitAddTorus.mFourierSubalgebra_coe, TemperedDistribution.smulLeftCLM_compL_smulLeftCLM, CStarModule.normedSpaceCore, continuousWithinAt_log_of_re_neg_of_im_zero, continuous_sin, exp_eq_exp_ℂ, PeriodPair.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept, PeriodPair.weierstrassP_coe, hasStrictFDerivAt_exp_real, ModularForm.prod_slash, MeasureTheory.ComplexMeasure.HaveLebesgueDecomposition.imPart, isQuotientCoveringMap_npow, WithCStarModule.prod_norm_sq, sum_cauchyPowerSeries_eq_integral, NumberField.mixedEmbedding.instIsAddHaarMeasureMixedSpaceVolume, CStarModule.innerSL_apply, DirichletCharacter.LSeries_twist_vonMangoldt_eq, Real.vector_fourierIntegral_eq_integral_exp_smul, cfc_complex_eq_real, UnitAddTorus.mFourierSubalgebra_closure_eq_top, Real.fourier_real_eq_integral_exp_smul, deriv_cos, CStarAlgebra.span_nonneg_inter_unitBall, not_differentiableAt_Gamma_neg_nat, AddCircle.homeomorphCircle'_symm_apply, isSelfAdjoint_iff_isStarNormal_and_spectrumRestricts, MeasureTheory.Lp.instFourierInvSMul, continuous_const_cpow, tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support, NumberField.mixedEmbedding.commMap_apply_of_isComplex, WithCStarModule.inner_def, hasSum_nat_jacobiTheta, NumberField.InfinitePlace.Completion.norm_coe, Real.fourier_deriv, differentiableOn_iteratedDerivWithin_cotTerm, PeriodPair.hasSum_derivWeierstrassPExcept, rotation_apply, toMatrix_rotation, differentiableAt_GammaAux, gelfandStarTransform_naturality, ModularForm.prod_slash_sum_weights, gelfandStarTransform_apply_apply, HarmonicAt.analyticAt_complex_partial, instPathConnectedSpaceUnits, Real.nnnorm_exp_I_mul_ofReal_sub_one_le, WeakFEPair.h_feq, continuousOn_cos, ZMod.completedLFunction_def_even, SchwartzMap.integral_fourierInv_smul_eq, summableLocallyUniformlyOn_iteratedDerivWithin_cotTerm, isOpen_slitPlane, DirichletCharacter.deriv_LFunction_eq_deriv_LSeries, MeasureTheory.SignedMeasure.toComplexMeasure_apply, CStarMatrix.toCLM_injective, integral_circleTransform, StrongFEPair.differentiable_Λ, Polynomial.toAddCircle_X_pow_eq_fourier, gelfandTransform_bijective, SchwartzMap.integral_bilin_fourierIntegral_eq, Real.fourierIntegral_continuousMultilinearMap_apply, NumberField.mixedEmbedding.polarSpaceCoord_target, OnePoint.isZeroAt_iff_exists_SL2Z, NumberField.mixedEmbedding.negAt_apply_snd, VectorFourier.fourierPowSMulRight_eq_comp, tendsto_exp_nhds_zero_iff, fourier_norm, uniformContinuous_im, frontier_preimage_re, CuspForm.coe_trace, image_circleMap_Ioc, NumberField.InfinitePlace.coe_apply, TemperedDistribution.smulLeftCLM_neg, reCLM_nnnorm, UpperHalfPlane.coe_pos_real_smul, Unitization.instStarOrderedRing, instContinuousStar, Function.HasTemperateGrowth.toTemperedDistribution_apply, NumberField.mixedEmbedding.negAt_preimage, hasDerivAt_GammaIntegral, deriv_ofReal_cpow_const, UpperHalfPlane.comp_ofComplex, starConvex_ofReal_slitPlane, analyticOnNhd_univ_iff_differentiable, SchwartzMap.integral_sesq_fourier_eq, NumberField.mixedEmbedding.fundamentalCone.volume_frontier_normLeOne, Real.fderiv_fourier, CStarMatrix.norm_def', NumberField.mixedEmbedding.iUnion_negAt_plusPart_ae, HurwitzZeta.hasSum_nat_sinZeta, isometry_conj, StrongFEPair.functional_equation, UnitDisc.coe_smul_circle, summable_conj, VectorFourier.fourierIntegral_continuousLinearMap_apply, GaussianFourier.integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace, continuousAt_arg, PeriodPair.latticeBasis_zero, ZMod.LFunction_def_odd, circleIntegral.integral_sub_inv_smul_sub_smul, SchwartzMap.fourier_lineDerivOp_eq, starConvex_one_slitPlane, TemperedDistribution.instLineDerivLeftSMulReal, CStarMatrix.inner_toCLM_conjTranspose_left, interior_setOf_le_re, Filter.tendsto_ofReal_iff, NumberField.mixedEmbedding.stdBasis_apply_isComplex_snd, TemperedDistribution.fourierInv_lineDerivOp_eq, UpperHalfPlane.mdifferentiable_inv_denom, hasStrictFDerivAt_cpow', NumberField.mixedEmbedding.negAt_signSet_apply_isComplex, NumberField.mixedEmbedding.fundamentalCone.volume_interior_eq_volume_closure, Real.fourier_iteratedFDeriv, Orientation.kahler_eq_zero_iff, AddChar.sum_apply_eq_ite, PositiveLinearMap.preGNS_norm_def, PositiveLinearMap.leftMulMapPreGNS_apply, UpperHalfPlane.dist_eq_iff_eq_sinh, integral_comp_polarCoord_symm, uniformContinuous_re, PeriodPair.ω₂_div_two_notMem_lattice, UnitAddTorus.mFourierCoeff_toLp, HurwitzZeta.differentiable_expZeta_of_ne_zero, PeriodPair.hasSum_derivWeierstrassP, NumberField.mixedEmbedding.fundamentalCone.smul_mem_of_mem, PeriodPair.compl_lattice_diff_singleton_mem_nhds, NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq, ext_inner_map, integrableOn_Ioi_cpow_iff, mellin_hasDerivAt_of_isBigO_rpow, HurwitzZeta.differentiable_hurwitzZetaOdd, ProbabilityTheory.integrable_rpow_abs_mul_cexp_of_re_mem_interior_integrableExpSet, LSeries_deriv_eqOn, TemperedDistribution.instFourierAdd, HurwitzZeta.differentiable_hurwitzZeta_sub_hurwitzZeta, PeriodPair.hasSumLocallyUniformly_derivWeierstrassP, sameRay_of_arg_eq, NumberField.mixedEmbedding.normAtComplexPlaces_polarSpaceCoord_symm, MeasureTheory.ComplexMeasure.singularPart_add_withDensity_rnDeriv_eq, UpperHalfPlane.ofComplex_apply_of_im_nonpos, Orientation.kahler_swap, NumberField.tendsto_sub_one_mul_dedekindZeta_nhdsGT, IsOpen.reProdIm, PeriodPair.hasFPowerSeriesAt_derivWeierstrassPExcept, frontier_setOf_im_lt, cauchyPowerSeries_apply, ModularFormClass.continuous, ContinuousLinearMap.instStarOrderedRing, CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM, TemperedDistribution.instFourierSMul, isConnected_of_lowerHalfPlane, HurwitzZeta.hasSum_hurwitzZeta_of_one_lt_re, NumberField.mixedEmbedding.fundamentalCone.logMap_expMapBasis, tendsto_exp_comap_re_atTop, convex_halfSpace_re_le, reCLM_coe, VectorFourier.hasFDerivAt_fourierIntegral, deriv_Gamma_add_one, CompletelyPositiveMap.instLinearMapClassComplex, ArithmeticFunction.vonMangoldt.continuousOn_LFunctionResidueClassAux', continuous_re, NumberField.InfinitePlace.Completion.isometry_extensionEmbedding, VectorFourier.fourierIntegral_iteratedFDeriv, UpperHalfPlane.contMDiff_coe, CuspForm.holo', PeriodPair.mem_lattice, BoundedContinuousFunction.mem_charPoly, spectrum.gelfandTransform_eq, Orientation.kahler_comp_rightAngleRotation, BoundedContinuousFunction.charAlgHom_apply, ArithmeticFunction.vonMangoldt.residueClass_apply, TemperedDistribution.delta_apply, MeasureTheory.memLp_haarAddCircle_iff, Circle.arg_eq_arg, PeriodPair.analyticOnNhd_derivWeierstrassPExcept, UpperHalfPlane.dist_eq_iff_eq_sq_sinh, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply_coe, NumberField.mixedEmbedding.convexBodySum_compact, Unitary.norm_sub_one_lt_two_iff, iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow, Real.circleAverage_eq_circleIntegral, comap_exp_nhds_zero, equivRealProdCLM_symm_apply, TemperedDistribution.instContinuousFourier, cos_eq_tsum', mellinInv_eq_fourierIntegralInv, cot_series_rep', DirichletCharacter.differentiableAt_LFunction, NumberField.canonicalEmbedding.integralBasis_repr_apply, interior_preimage_re, continuous_cosh, fourier_one, PositiveLinearMap.instContinuousLinearMapClassComplexOfLinearMapClassOfOrderHomClass, NumberField.mixedEmbedding.fundamentalCone.subset_interior_normLeOne, NumberField.canonicalEmbedding.integerLattice.inter_ball_finite, PeriodPair.basis_zero, UpperHalfPlane.image_coe_ball, NumberField.ComplexEmbedding.IsConj.eq, NumberField.mixedEmbedding.negAt_signSet_apply_isReal, closure_setOf_lt_im, Real.Angle.coe_toCircle, tendsto_integral_exp_smul_cocompact, hasDerivAt_Gammaℝ_one, hasSum_jacobiTheta₂_term, hasFDerivAt_jacobiTheta₂_term, continuousAt_cpow_const_of_re_pos, Real.fourierIntegral_continuousLinearMap_apply, LSeries_deriv, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, UpperHalfPlane.contMDiff_inv_denom, gelfandStarTransform_symm_apply, uniformlyContinuous_re, map_exp_comap_re_atTop, differentiable_exp, UnitDisc.isEmbedding_coe, HurwitzZeta.hasSum_nat_completedCosZeta, tendsto_sub_mul_tsum_nat_cpow, Polynomial.toAddCircle.integrable, fourier_zero, fourier_neg', Function.Periodic.boundedAtFilter_cuspFunction, Summable_cotTerm, SchwartzMap.delta_apply, norm_cauchyPowerSeries_le, mellinInv_eq_fourierInv, summable_jacobiTheta₂_term_fderiv_iff, HurwitzZeta.hasSum_nat_hurwitzZetaEven, VectorFourier.fourierIntegral_const_smul, HurwitzZeta.hasSum_int_cosKernel, ZMod.completedLFunction_def_odd, Real.fourier_real_eq, OnePoint.isZeroAt_infty_iff, Circle.smul_def, hasSum_fourier_series_L2, NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis, PeriodPair.isClosed_lattice, IsSelfAdjoint.val_re_map_spectrum, realPart.norm_le, BoundedContinuousFunction.innerProbChar_zero, tendsto_normSq_cocompact_atTop, NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIdealLattice, Real.tendsto_integral_gaussian_smul', Real.hasFDerivAt_fourier, HurwitzZeta.hurwitzZeta_neg_nat, convex_halfSpace_im_gt, EisensteinSeries.tendsto_zero_inv_linear_sub, GaussianFourier.integrable_cexp_neg_mul_sum_add, continuousOn_sin, hasStrictFDerivAt_cpow, tendsto_riemannZeta_sub_one_div, ZetaAsymptotics.tendsto_Gamma_term_aux, NumberField.InfinitePlace.Completion.locallyCompactSpace, polarCoord_apply, Real.fourierIntegral_convergent_iff', differentiable_iteratedDeriv_sin, AddChar.expect_apply_eq_zero_iff_ne_zero, hasStrictDerivAt_sinh, inner_map_polarization', EisensteinSeries.linear_right_summable, UnitAddTorus.mFourier_add, PositiveLinearMap.preGNS_inner_def, CStarAlgebra.instNonnegSpectrumClassComplexNonUnital, UpperHalfPlane.cosh_dist, LSeries_eq_mul_integral_of_nonneg, UpperHalfPlane.image_coe_closedBall, PeriodPair.periodic_derivWeierstrassP, EisensteinSeries.summable_linear_left_mul_linear_left, tendsto_one_add_div_pow_exp, spectrum.gelfand_formula, NumberField.InfinitePlace.Completion.isClosed_image_extensionEmbedding, riemannZeta_eulerProduct_exp_log, IsSelfAdjoint.isConnected_spectrum_compl, VectorFourier.iteratedFDeriv_fourierIntegral, UpperHalfPlane.dist_coe_center, MeasureTheory.ComplexMeasure.equivSignedMeasure_apply, tendsto_arg_nhdsWithin_im_nonneg_of_re_neg_of_im_zero, HarmonicAt.differentiableAt_complex_partial, tendsto_logDeriv_euler_sin_div, EisensteinSeries.div_linear_zpow_differentiableOn, UnitAddTorus.mFourier_zero, Real.fourierIntegral_iteratedDeriv, CStarAlgebra.span_nonneg_inter_unitClosedBall, UpperHalfPlane.ofComplex_apply_of_im_pos, NumberField.mixedEmbedding.span_idealLatticeBasis, NumberField.mixedEmbedding.fundamentalCone.norm_expMapBasis, VonNeumannAlgebra.centralizer_centralizer', StarAlgebra.elemental.bijective_characterSpaceToSpectrum, antilipschitz_equivRealProd, zeta_eq_tsum_one_div_nat_cpow, isometry_ofReal, continuousAt_cpow, gelfandTransform_map_star, NumberField.mixedEmbedding.convexBodySumFun_smul, interior_preimage_im, NumberField.mixedEmbedding.logMap_real_smul, isBigO_re_sub_re, AddChar.sum_apply_eq_zero_iff_ne_zero, comap_exp_nhdsNE, WeakFEPair.Λ₀_eq, UnitAddTorus.coeFn_mFourierLp, NumberField.mixedEmbedding.polarCoord_symm_apply, NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal_coe, deriv_Gamma_nat, UpperHalfPlane.lt_dist_iff_lt_dist_coe_center, spectrum.map_pow, cfcₙ_real_eq_complex, NumberField.InfinitePlace.isInfinitePlace, continuous_sinh, UnitDisc.coe_closedBall_smul, selfAdjoint.unitarySelfAddISMul_coe, Circle.ext_iff, TemperedDistribution.fourier_toTemperedDistributionCLM_eq, isOpen_compl_range_intCast, nhdsWithin_lt_le_nhdsWithin_stolzSet, hasSum_ofReal, CuspFormClass.zero_at_infty, HurwitzZeta.completedHurwitzZetaEven_residue_one, ofRealCLM_nnnorm, imCLM_norm, hasDerivAt_jacobiTheta₂_fst, ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div, UnitAddTorus.mFourier_neg, VectorFourier.fourierIntegral_convergent_iff, continuousOn_norm_circleTransformBoundingFunction, continuousAt_Gamma_one, intervalIntegral.intervalIntegrable_cpow, PeriodPair.differentiableOn_derivWeierstrassP, hasDerivAt_sinh, PeriodPair.weierstrassPExcept_def, NumberField.InfinitePlace.smul_coe_apply, HurwitzZeta.hasSum_int_cosZeta, WeakFEPair.h_feq', SchwartzMap.convolution_apply, hasSum_jacobiTheta₂_term_fderiv, NumberField.mixedEmbedding.mem_span_latticeBasis, ZetaAsymptotics.tendsto_riemannZeta_sub_one_div_Gammaℝ, tendsto_norm_tan_atTop, TemperedDistribution.fourierTransformInv_toTemperedDistributionCLM_eq, BoundedContinuousFunction.innerProbChar_apply, Circle.coe_inv_eq_conj, hasDerivAt_Gammaℂ_one, AnalyticAt.eventually_constant_or_nhds_le_map_nhds, hasSum_sin, tendsto_self_mul_Gamma_nhds_zero, SchwartzMap.integral_bilin_fourier_eq, hasStrictDerivAt_const_cpow, PositiveLinearMap.toPreGNS_ofPreGNS, Orientation.kahler_neg_orientation, IsSelfAdjoint.cfc_arg, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius, intervalIntegral.integrableOn_Ioo_cpow_iff, SchwartzMap.fourierInv_apply_eq, Circle.coe_mul, UpperHalfPlane.dist_lt_iff_dist_coe_center_lt, hasSum_jacobiTheta₂'_term, NumberField.mixedEmbedding.negAt_apply_isReal_and_notMem, circleIntegral.norm_two_pi_i_inv_smul_integral_le_of_norm_le_const, lipschitzWith_circleMap, tendsto_arg_nhdsWithin_im_neg_of_re_neg_of_im_zero, circleMap_notMem_ball, SchwartzMap.toTemperedDistributionCLM_apply_apply, SlashInvariantFormClass.periodic_comp_ofComplex, integrableOn_Ioi_deriv_ofReal_cpow, HurwitzZeta.hurwitzZetaOdd_neg_two_mul_nat, PositiveLinearMap.exists_norm_apply_le, Real.fourierIntegral_real_eq_integral_exp_smul, map_exp_comap_re_atBot, fourier_coe_apply, Real.deriv_fourierIntegral, interior_setOf_le_im, fourierSubalgebra_separatesPoints, isEquivalent_sinh, AnalyticOnNhd.is_constant_or_isOpenMap, Real.Angle.arg_toCircle, MeasureTheory.SignedMeasure.re_toComplexMeasure, TemperedDistribution.smulLeftCLM_sub, one_add_cpow_hasFPowerSeriesAt_zero, HurwitzZeta.hasSum_nat_cosZeta, fourierCoeff.const_smul, NumberField.mixedEmbedding.volume_preserving_negAt, OnePoint.isZeroAt_iff_forall_SL2Z, hasSum_cauchyPowerSeries_integral, Circle.coe_pow, MeasureTheory.Lp.instFourierSMul, UpperHalfPlane.contMDiff_num, UpperHalfPlane.mdifferentiable_denom, UpperHalfPlane.dist_self_center, continuous_conj, Function.locallyFinsuppWithin.toClosedBall_divisor, LSeries.term_convolution, MeasureTheory.ComplexMeasure.integrable_rnDeriv, NumberField.mixedEmbedding.negAt_apply_isComplex, isBigO_riemannZeta_sub_one_div, hasFDerivAt_cpow, differentiableAt_exp, fourierIntegral_eq_half_sub_half_period_translate, not_continuousAt_Gamma_zero, differentiable_Gammaℝ_inv, continuous_circleMap, differentiableAt_jacobiTheta₂_fst, iter_deriv_exp, HasProdLocallyUniformlyOn_euler_sin_prod, NormedSpace.ofReal_exp_ℝ_ℝ, convex_halfSpace_im_lt, Polynomial.rootSet_derivative_subset_convexHull_rootSet, VonNeumannAlgebra.mem_carrier, differentiableAt_tan, has_antideriv_at_fourier_neg, UnitAddTorus.mFourier_norm, CStarModule.norm_inner_le, VonNeumannAlgebra.centralizer_centralizer, NumberField.mixedEmbedding.normAtComplexPlaces_normAtAllPlaces, LSeriesSummable.sum, Function.Periodic.continuous_qParam, HurwitzZeta.hasSum_expZeta_of_one_lt_re, UniformContinuousOn.cexp, continuous_exp, HurwitzZeta.hasSum_int_completedHurwitzZetaOdd, StarSubalgebra.spectrum_eq, frontier_preimage_im, one_div_sub_sq_hasFPowerSeriesOnBall_zero, DirichletCharacter.summable_neg_log_one_sub_mul_prime_cpow, continuousAt_clog, EisensteinSeries.linear_left_summable, PeriodPair.hasSumLocallyUniformly_weierstrassPExcept, Circle.invOn_arg_exp, hasDerivAt_cos, ofRealCLM_apply, UpperHalfPlane.ofComplex_apply_eq_of_im_nonpos, log_sub_self_isBigO, differentiableAt_complex_iff_differentiableAt_real, cfcHom_real_eq_restrict, NumberField.mixedEmbedding.mem_negAt_plusPart_of_mem, CStarAlgebra.norm_smul_two_inv_smul_add_four_unitary, inner_map_complex, BoundedContinuousFunction.probCharDual_zero, arg_eq_nhds_of_im_neg, CStarMatrix.toCLM_apply_single, hasSum_two_pi_I_cauchyPowerSeries_integral, Real.fourier_fderiv, tendsto_exp_comap_re_atBot, IsSelfAdjoint.spectrumRestricts, NumberField.mixedEmbedding.fundamentalCone.closure_normLeOne_subset, imaginaryPart.norm_le, Polynomial.eq_centerMass_of_eval_derivative_eq_zero, VectorFourier.integral_sesq_fourierIntegral_eq_neg_flip, tsum_riemannZetaSummand, restrictScalars_one_smulRight, summable_ofReal, one_div_one_sub_pow_hasFPowerSeriesOnBall_zero, hasDerivAt_fourier_neg, VectorFourier.fderiv_fourierIntegral, AnalyticAt.harmonicAt_conj, fourier_eval_zero, SchwartzMap.fourierInv_lineDerivOp_eq, VectorFourier.integral_fourierIntegral_swap, tendsto_euler_sin_prod, ZMod.completedLFunction_eq, hasStrictDerivAt_log, linear_isometry_complex, CFC.log_monotoneOn, NumberField.mixedEmbedding.convexBodySumFun_continuous, Fourier.fourierIntegral_const_smul, CStarMatrix.toCLM_apply_eq_sum, UpperHalfPlane.dist_eq, Circle.star_addChar, HurwitzZeta.hurwitzZeta_residue_one, WithCStarModule.pi_norm, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_mem_fundamentalCone_iff, fourierCoeff_toLp, IsSelfAdjoint.toReal_spectralRadius_complex_eq_norm, ProbabilityTheory.hasDerivAt_complexMGF, tsum_exp_neg_quadratic, CFC.monotone_rpow, PeriodPair.derivWeierstrassP_sub_coe, isAddQuotientCoveringMap_exp, inr_comp_cfcₙHom_eq_cfcₙAux, rotationOf_rotation, CFC.monotoneOn_one_sub_one_add_inv_real, SpectrumRestricts.real_iff, HurwitzZeta.differentiableAt_completedHurwitzZetaEven, cosh_eq_tsum, NumberField.mixedEmbedding.volume_preserving_mixedSpaceToRealMixedSpace_symm, frontier_setOf_lt_im, CStarMatrix.ofMatrix_eq_ofMatrixL, interior_reProdIm, HurwitzZeta.differentiableAt_one_completedHurwitzZetaEven_sub_completedHurwitzZetaEven, CommCStarAlgebra.toStarModule, contDiff_exp, Real.fourier_eq, closure_preimage_re, isOpenQuotientMap_pow, HurwitzZeta.hasSum_int_sinKernel, SchwartzMap.fourier_evalCLM_eq, interior_setOf_im_le, NumberField.canonicalEmbedding.nnnorm_eq, QuasispectrumRestricts.real_iff, TemperedDistribution.instLineDerivSMulReal, cot_series_rep, UpperHalfPlane.ofComplex_apply_eq_ite, MeasureTheory.Measure.toTemperedDistribution_apply, tendsto_integral_exp_smul_cocompact_of_inner_product, HurwitzZeta.completedCosZeta_residue_zero, CStarMatrix.toCLM_apply, UpperHalfPlane.qParam_tendsto_atImInfty, isConnected_of_upperHalfPlane, differentiable_sin, UpperHalfPlane.dist_eq_iff_dist_coe_center_eq, continuous_normSq, PeriodPair.weierstrassP_add_coe, NumberField.mixedEmbedding.stdBasis_apply_isComplex_fst, TemperedDistribution.fourier_lineDerivOp_eq, PeriodPair.instProperSpaceSubtypeComplexMemSubmoduleIntLattice, circleMap_mem_sphere, selfAdjoint.realPart_unitarySelfAddISMul, hasDerivAt_logTaylor, DirichletCharacter.differentiable_LFunction, HurwitzZeta.hurwitzZetaEven_one_sub_two_mul_nat, iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow, NumberField.mixedEmbedding.norm_smul, circleMap_preimage_codiscrete, PositiveLinearMap.gnsStarAlgHom_apply, Real.fourier_iteratedDeriv, lintegral_comp_polarCoord_symm, NumberField.mixedEmbedding.fundamentalDomain_stdBasis, NumberField.mixedEmbedding.span_latticeBasis, zero_cpow_eq_nhds, WeakFEPair.hf_zero, spectrum.nonempty, Circle.leftInverse_exp_arg, continuousAt_ofReal_cpow, AnalyticAt.eventually_constant_or_nhds_le_map_nhds_aux, circleMap_mem_closedBall, LinearMap.isPositive_iff_complex, VectorFourier.fourierSMulRight_apply, UnitAddTorus.instContinuousSMulComplexSubtypeAEEqFunVolumeMemAddSubgroupLp, TemperedDistribution.lineDerivOp_toTemperedDistributionCLM_eq, NumberField.mixedEmbedding.polarCoord_source, isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts, UpperHalfPlane.J_smul, HurwitzZeta.sinZeta_two_mul_nat_add_one', UpperHalfPlane.cmp_dist_eq_cmp_dist_coe_center, hasDerivAt_circleMap, instNonemptyElemWeakDualComplexCharacterSpaceOfNontrivial, UnitDisc.instSMulCommClass_closedBall_right, UnitAddTorus.hasSum_mFourier_series_L2, CFC.rpow_le_rpow, TemperedDistribution.laplacian_eq_sum, NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul, WithCStarModule.pi_inner, NumberField.mixedEmbedding.continuous_norm, MeasureTheory.ComplexMeasure.HaveLebesgueDecomposition.rePart, continuousOn_tan, TemperedDistribution.instContinuousLineDeriv, RCLike.complexLinearIsometryEquiv_symm_apply, WithCStarModule.prod_norm, hasDerivAt_fourier, Filter.Tendsto.ofReal, continuousAt_cpow_zero_of_re_pos, Circle.norm_coe, NumberField.mixedEmbedding.polarSpaceCoord_symm_apply, spectrum.limsup_pow_nnnorm_pow_one_div_le_spectralRadius, measurableEquivRealProd_symm_polarCoord_symm_apply, UnitDisc.instIsScalarTower_closedBall, NumberField.mixedEmbedding.fundamentalCone.norm_normAtAllPlaces, instCompleteSpace, ZMod.LFunction_def_even, Real.fourier_bilin_convolution_eq, UpperHalfPlane.le_dist_coe, one_div_sub_pow_hasFPowerSeriesOnBall_zero, CStarMatrix.mul_entry_mul_eq_inner_toCLM, ModularFormClass.differentiableAt_cuspFunction, fourier_apply, QuadraticForm.equivalent_sum_squares, HurwitzZeta.hasSum_nat_completedSinZeta, integrableOn_exp_mul_complex_Iic, SchwartzMap.integral_sesq_fourierIntegral_eq, Real.fourierIntegral_eq', frontier_setOf_le_re, CStarModule.norm_sq_eq, hasFPowerSeriesOn_cauchy_integral, UpperHalfPlane.contMDiff_denom_zpow, convex_halfSpace_re_ge, deriv_circleMap, PeriodPair.latticeBasis_one, NormedRing.algEquivComplexOfComplete_symm_apply, VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral', NonUnitalCommCStarAlgebra.toStarModule, hasStrictDerivAt_cos, Orientation.kahler_apply_self, frontier_setOf_re_lt, IsPrimitiveRoot.nnnorm_eq_one, PeriodPair.weierstrassP_sub_coe, analyticOn_univ_iff_differentiable, Unitary.spectrum_subset_slitPlane_iff_norm_lt_two, conjCLE_nnorm, NumberField.mixedEmbedding.mixedSpaceToRealMixedSpace_apply, MeasureTheory.SignedMeasure.toComplexMeasure_apply_re, isBigO_im_sub_im, ArithmeticFunction.LSeries_vonMangoldt_eq, WithCStarModule.inner_single_right, Real.iteratedDeriv_fourier, isCoveringMapOn_exp, selfAdjoint.star_coe_unitarySelfAddISMul, Orientation.kahler_rotation_left', zeta_eq_tsum_one_div_nat_add_one_cpow, continuous_cos, DirichletCharacter.differentiableAt_completedLFunction, NumberField.mixedEmbedding.euclidean.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, convex_halfSpace_im_ge, rotation_trans, CStarAlgebra.rpow_neg_one_le_rpow_neg_one, UpperHalfPlane.le_dist_iff_le_dist_coe_center, NumberField.mixedEmbedding.polarCoord_target, continuousAt_arg_coe_angle, NumberField.mixedEmbedding.normAtPlace_polarCoord_symm_of_isReal, PeriodPair.hasSum_weierstrassP, convex_halfSpace_re_lt, NumberField.count_multisetInfinitePlace_eq_mult, UpperHalfPlane.ofComplex_apply, NumberField.mixedEmbedding.euclidean.instIsZLatticeRealMixedSpaceIntegerLattice, TemperedDistribution.smulLeftCLM_add, PeriodPair.coeff_weierstrassPSeries, ball_one_subset_slitPlane, PeriodPair.isOpen_compl_lattice_diff, restrictScalars_toSpanSingleton, Orientation.normSq_kahler, volume_closedBall, UnitDisc.mk_neg, tendsto_one_add_div_cpow_exp, hasSum_cos', closure_setOf_re_lt, deriv_cosh, PeriodPair.derivWeierstrassP_coe, NumberField.InfinitePlace.Completion.extensionEmbedding_coe, NumberField.mixedEmbedding.negAt_symm, LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_and_nonneg, fourierSubalgebra_coe, NumberField.InfinitePlace.denseRange_algebraMap_pi, Polynomial.toAddCircle_monomial_eq_smul_fourier, inner, continuousAt_const_cpow', hasStrictDerivAt_sin, polarCoord_source, MulChar.star_apply', NumberField.mixedEmbedding.polarCoord_symm_eq, exp_sub_sum_range_succ_isLittleO_pow, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, continuousOn_prod_circle_transform_function, ProbabilityTheory.integrable_cexp_mul_of_re_mem_interior_integrableExpSet, NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIntegerLattice, HasDerivAt.ofReal_comp, UpperHalfPlane.dist_center_dist, DifferentiableAt.ofReal_cpow_const, NumberField.mixedEmbedding.negAt_apply_isReal_and_mem, hasFDerivAt_jacobiTheta₂, isHomeomorphicTrivialFiberBundle_re, NumberField.mixedEmbedding.polarSpaceCoord_target', rotationOf_coe, NumberField.mixedEmbedding.volume_negAt_plusPart, deriv_tan, NumberField.InfinitePlace.isometry_embedding_of_isReal, UpperHalfPlane.dist_le_dist_coe_div_sqrt, hasDerivAt_cosh, EisensteinSeries.tendsto_zero_inv_linear, Unitization.nnreal_cfcₙ_eq_cfc_inr, NumberField.ComplexEmbedding.place_conjugate, UnitDisc.coe_smul_closedBall, HurwitzZeta.differentiableAt_hurwitzZeta, NumberField.inverse_basisMatrix_mulVec_eq_repr, TemperedDistribution.fourierTransform_apply, interior_setOf_re_le, DirichletCharacter.deriv_LFunctionTrivChar₁_apply_of_ne_one, isOpen_im_gt_EReal, CStarModule.norm_eq_csSup, tendsto_logDeriv_euler_cot_sub, SlashInvariantForm.coe_trace, isConformalMap_complex_linear_conj, NumberField.mixedEmbedding.iUnion_negAt_plusPart_union, LSeries_differentiableOn, IsSelfAdjoint.spectralRadius_eq_nnnorm, differentiableAt_riemannZeta, tendsto_partialGamma, exp_sub_sum_range_isBigO_pow, tendsto_norm_tan_of_cos_eq_zero, riemannZeta_eulerProduct, isOpenQuotientMap_zpow_compl_zero, UpperHalfPlane.eventuallyEq_coe_comp_ofComplex, EisensteinSeries.summable_linear_sub_mul_linear_add, Orientation.kahler_rightAngleRotation_left, Orientation.kahler_comp_linearIsometryEquiv, HurwitzZeta.hasSum_nat_hurwitzZetaOdd, Real.fourierIntegral_fderiv, Function.Periodic.invQParam_tendsto, cfcₙHom_real_eq_restrict, PeriodPair.latticeEquiv_symm_apply, MeasureTheory.ComplexMeasure.im_apply, closure_setOf_lt_re, UnitAddTorus.mFourierSubalgebra_separatesPoints, betaIntegral_convergent, Real.fourierIntegral_convergent_iff, NumberField.canonicalEmbedding.mem_rat_span_latticeBasis, PeriodPair.hasSumLocallyUniformly_derivWeierstrassPExcept, LSeries_sum, UpperHalfPlane.comp_ofComplex_of_im_le_zero, hasDerivAt_sin, fourierCoeff_eq_intervalIntegral, NumberField.mixedEmbedding.continuous_normAtPlace, closure_reProdIm, Real.hasDerivAt_fourierChar, WStarAlgebra.exists_predual, span_fourierLp_closure_eq_top, Orientation.kahler_rotation_left, multipliable_sineTerm, LindemannWeierstrass.integral_exp_mul_eval, ModularFormClass.hasSum_qExpansion_of_abs_lt, isUniformEmbedding_ofReal, conjCLE_enorm, DirichletCharacter.LSeries_eulerProduct_hasProd, hasSum_conj, PeriodPair.deriv_derivWeierstrassPExcept_self, WeakFEPair.functional_equation₀, NormedRing.algEquivComplexOfComplete_apply, CFC.nnrpow_le_nnrpow, Real.tendsto_integral_cexp_sq_smul, inner_map_self_eq_zero, hasStrictDerivAt_exp, Real.enorm_exp_I_mul_ofReal_sub_one_le, Real.iteratedFDeriv_fourier, SchwartzMap.convolution_continuous_left, IsStarNormal.instContinuousFunctionalCalculus, circleIntegral.integral_smul_const, hasStrictDerivAt_cosh, CStarAlgebra.span_nonneg_inter_closedBall, NumberField.mixedEmbedding.injective_mixedSpaceOfRealSpace, SchwartzMap.integral_fourier_mul_eq, continuousAt_cpow_const, GaussianFourier.tendsto_verticalIntegral, wedgeIntegral_add_wedgeIntegral_eq, UnitDisc.continuous_coe, HurwitzZeta.sinZeta_two_mul_nat_add_one, differentiableAt_const_cpow_of_neZero, tsum_dirichletSummand, Real.hasFDerivAt_fourierIntegral, linearEquiv_det_rotation, dist_conj_conj, circleIntegrable_sub_zpow_iff, Polynomial.fourierCoeff_toAddCircle_natCast, conjCLE_apply, Circle.coe_eq_one, differentiable_one_div_Gamma, UpperHalfPlane.cosh_half_dist, SchwartzMap.lineDerivOp_fourierInv_eq, NumberField.mixedEmbedding.stdBasis_apply_isReal, DirichletCharacter.LSeries_eulerProduct_exp_log, not_differentiableAt_Gamma_zero, Real.fourierChar_apply, NumberField.canonicalEmbedding.norm_le_iff, NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, StarSubalgebra.mem_spectrum_iff, ProbabilityTheory.differentiableOn_complexMGF, Real.fourier_bilin_convolution_eq_integral, PeriodPair.deriv_weierstrassPExcept_same, MeasureTheory.ComplexMeasure.equivSignedMeasureₗ_symm_apply, Function.Periodic.qParam_tendsto, continuousAt_jacobiTheta, PeriodPair.analyticOnNhd_derivWeierstrassP, Gammaℝ_residue_zero, integrableOn_Ioi_cpow_of_lt, EulerSine.antideriv_cos_comp_const_mul, instTietzeExtension, NumberField.mixedEmbedding.convexBodyLT_convex, Real.tendsto_integral_exp_smul_cocompact, instT2Space, mellin_convergent_iff_norm, UpperHalfPlane.exp_half_dist, Orientation.kahler_mul, GaussianFourier.integral_cexp_neg_mul_sum_add, continuous_ofReal_cpow_const, one_div_one_sub_cpow_hasFPowerSeriesOnBall_zero, NormedAlgebra.Real.nonempty_algEquiv_or, HurwitzZeta.differentiableAt_completedCosZeta, fourier_neg, LSeries.tendsto_cpow_mul_atTop, ArithmeticFunction.vonMangoldt.LSeries_residueClass_eq, WeakDual.CharacterSpace.mem_spectrum_iff_exists, sinh_eq_tsum, continuousAt_jacobiTheta₂, HurwitzZeta.hasSum_nat_hurwitzZetaEven_of_mem_Icc, Polynomial.isOpenQuotientMap_eval, NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIdealLattice, CStarAlgebra.rpow_neg_one_le_one, EulerSine.antideriv_sin_comp_const_mul, differentiableAt_cosh, differentiableAt_Gamma_nat_add_one, TemperedDistribution.instFourierInvSMul, PositiveLinearMap.ofPreGNS_toPreGNS, deriv_cos', imCLM_coe, WeakFEPair.hf_modif_FE, isQuotientMap_im, CStarMatrix.normedSpaceCore, circleAverage_log_norm_factorizedRational, ContinuousLinearMap.isPositive_iff_complex, fourierIntegral_half_period_translate, MeasureTheory.stronglyMeasurable_charFun, PeriodPair.instDiscreteTopologySubtypeComplexMemSubmoduleIntLattice, spectrum.pow_norm_pow_one_div_tendsto_nhds_spectralRadius, continuous_ofReal, Orientation.kahler_map, isBigO_deriv_ofReal_cpow_const_atTop, not_continuousAt_Gamma_neg_nat, TemperedDistribution.instFourierInvAdd, Polynomial.C_eq_or_isOpenQuotientMap_eval, hasDerivAt_ofReal_cpow_const, UnitAddTorus.hasSum_prod_mFourierCoeff, NumberField.mixedEmbedding.latticeBasis_apply, TemperedDistribution.fourierInv_apply, sin_eq_tsum, differentiableAt_jacobiTheta₂_snd, SchwartzMap.instFourierSMul, SchwartzMap.fourierTransformCLM_apply, NumberField.mixedEmbedding.measurable_polarCoord_symm, LSeries.tendsto_atTop, NumberField.InfinitePlace.Completion.extensionEmbedding_of_isReal_coe, TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq, one_add_cpow_hasFPowerSeriesOnBall_zero, SchwartzMap.fderivCLM_fourier_eq, CStarModule.inner_mul_inner_swap_le, hasSum_conj', isOpen_im_lt_EReal, TemperedDistribution.instLineDerivAdd, Circle.coe_inv, Polynomial.supNorm_le_choose_natDegree_div_two_mul_mahlerMeasure, hasStrictDerivAt_cpow_const, mellin_differentiableAt_of_isBigO_rpow_exp, hasSum_taylorSeries_neg_log, VectorFourier.integral_bilin_fourierIntegral_eq_flip, CFC.monotone_sqrt, NumberField.mixedEmbedding.logMap_real, NumberField.mixedEmbedding.commMap_apply_of_isReal, NormedSpace.of_real_exp_ℝ_ℝ, NumberField.mixedEmbedding.polarCoord_apply, TemperedDistribution.instLineDerivSMulComplex, ProbabilityTheory.integrable_pow_abs_mul_cexp_of_re_mem_interior_integrableExpSet, euler_sineTerm_tprod, ProbabilityTheory.integrable_pow_mul_cexp_of_re_mem_interior_integrableExpSet, ArithmeticFunction.vonMangoldt.continuousOn_LFunctionResidueClassAux, WeakFEPair.functional_equation, GaussianFourier.integrable_cexp_neg_mul_sq_norm_add, log_eq_integral, equivRealProdCLM_symm_apply_re, UpperHalfPlane.sinh_half_dist_add_dist, NumberField.mixedEmbedding.continuous_normAtAllPlaces, IsCompact.reProdIm, one_div_one_sub_sq_hasFPowerSeriesOnBall_zero, HurwitzZeta.differentiable_cosZeta_of_ne_zero, norm_cfcₙ_one_sub_one_add_inv_lt_one, NumberField.mixedEmbedding.latticeBasis_repr_apply, deriv_cpow_const, SchwartzMap.integral_fourierInv_mul_eq, Real.fourierIntegral_continuousLinearMap_apply', TemperedDistribution.laplacian_toTemperedDistributionCLM_eq, summable_one_div_nat_cpow, IsStarNormal.instNonUnitalIsometricContinuousFunctionalCalculus, nndist_conj_comm, VonNeumannAlgebra.coe_toStarSubalgebra, logDeriv_prod_sineTerm_eq_sum_cotTerm, differentiableAt_Gamma_one, Real.differentiable_fourierChar, NumberField.AdeleRing.algebraMap_fst_apply, VectorFourier.fourierPowSMulRight_apply, mdifferentiable_jacobiTheta, StarSubalgebra.coe_isUnit, WithCStarModule.inner_single_left, instProperSpace, NumberField.mixedEmbedding.normAtPlace_negAt, nndist_conj_conj, SchwartzMap.convolution_flip, isometryOfOrthonormal_apply, frontier_setOf_le_re_and_le_im, sameRay_iff, instContinuousMapUniqueHom, Circle.normSq_coe, hasDerivAt_Gamma_one, NumberField.mixedEmbedding.normAtPlace_smul, PeriodPair.hasSum_weierstrassPExcept, NumberField.mixedEmbedding.fundamentalCone.isBounded_normLeOne, ProbabilityTheory.hasDerivAt_iteratedDeriv_complexMGF, NumberField.mixedEmbedding.finrank, SchwartzMap.integral_fourier_smul_eq, imCLM_nnnorm, UpperHalfPlane.contMDiffAt_ofComplex, fourierSubalgebra_closure_eq_top, ModularForm.prod_fintype_slash, GaussianFourier.integral_cexp_neg_sum_mul_add, selfAdjoint.val_re_map_spectrum, NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply, circleIntegrable_sub_inv_iff, ModularFormClass.bounded_at_infty_comp_ofComplex, NumberField.mixedEmbedding.convexBodySum_isBounded, Unitization.complex_cfcₙ_eq_cfc_inr, sameRay_iff_arg_div_eq_zero, arg_eq_nhds_of_im_pos, ModularForm.holo', NumberField.mixedEmbedding.polarSpaceCoord_apply, Real.nonempty_algEquiv_or, starConvex_slitPlane, VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral, NumberField.mixedEmbedding.negAt_apply_norm_isReal, log_sub_logTaylor_isBigO, differentiable_completedZeta₀, fourier_zero', HurwitzZeta.hasSum_int_sinZeta, CFC.log_le_log, differentiable_sinh, ZMod.toCircle_intCast, iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum, ArithmeticFunction.LSeries_zeta_eulerProduct_exp_log, ZMod.toCircle_natCast, inner_map_polarization, ModularFormClass.hasSum_qExpansion_of_norm_lt, volume_ball, Real.deriv_fourierChar, TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq, Real.iteratedFDeriv_fourierIntegral, cpow_eq_nhds', jacobiTheta_eq_tsum_nat, PositiveLinearMap.norm_apply_le_of_nonneg, UnitDisc.instSMulCommClass_circle_closedBall, differentiable_iteratedDeriv_sinh, LSeries.term_sum_apply, nnnorm_intCast, NumberField.InfinitePlace.Completion.isometry_extensionEmbedding_of_isReal, UpperHalfPlane.contMDiffAt_iff, Orientation.kahler_apply_apply, NonUnitalCStarAlgebra.toIsScalarTower, nhdsWithin_stolzCone_le_nhdsWithin_stolzSet, VonNeumannAlgebra.mem_commutant_iff, VectorFourier.fourierIntegral_continuousMultilinearMap_apply, differentiableAt_sinh, hasDerivAt_ofReal_cpow_const', hasDerivAt_Gamma_one_half, Function.Periodic.differentiable_qParam, continuous_tan, CFC.sqrt_le_sqrt, MeasureTheory.ComplexMeasure.absolutelyContinuous_ennreal_iff, PeriodPair.differentiableOn_weierstrassPExcept, Real.differentiable_fourierChar_neg_bilinear_right, conjCLE_norm, MeasureTheory.Lp.ker_toTemperedDistributionCLM_eq_bot, MeasureTheory.Lp.toTemperedDistribution_toLp_eq, differentiableAt_log, differentiableAt_completedZeta, PeriodPair.derivWeierstrassPExcept_add_coe, isQuotientMap_re, Circle.coeHom_apply, Real.tendsto_integral_gaussian_smul, dist_conj_comm, CStarModule.continuous_inner, rootsOfUnityCircleEquiv_apply, CuspFormClass.zero_at_infty_slash, subfield_eq_of_closed, VectorFourier.fourierIntegral_comp_add_right, PeriodPair.differentiableOn_weierstrassP, UnitAddTorus.span_mFourier_closure_eq_top, TemperedDistribution.laplacian_apply_apply, imCLM_enorm, TemperedDistribution.smulLeftCLM_smulLeftCLM_apply, tendsto_integral_exp_inner_smul_cocompact, det_rotation, UpperHalfPlane.mdifferentiable_coe, Circle.coe_inj, arg_eq_nhds_of_re_pos, integral_complex_ofReal, VectorFourier.fourierIntegral_probChar, summable_cotTerm, continuousAt_jacobiTheta₂', IsSelfAdjoint.self_add_I_smul_cfcSqrt_sub_sq_mem_unitary, NonUnitalCommCStarAlgebra.toSMulCommClass, RCLike.toContinuousLinearMap_complexLinearIsometryEquiv, EisensteinSeries.eisSummand_extension_differentiableOn, Orientation.kahler_rotation_right, ofRealCLM_enorm, Fourier.fourierIntegral_def, isOpenQuotientMap_pow_compl_zero, deriv_sinh, NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis, TemperedDistribution.lineDerivOp_apply_apply, MeasureTheory.ComplexMeasure.re_apply, intervalIntegral.intervalIntegrable_cpow', deriv_sin, Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv, fourier_coe_apply', NumberField.mixedEmbedding.polarSpaceCoord_source, cfc_real_eq_complex, TemperedDistribution.lineDerivOp_fourierInv_eq, hasSum_taylorSeries_log, fourierCoeffOn_eq_integral, VonNeumannAlgebra.coe_commutant, UpperHalfPlane.dist_coe_le, spectrum.exists_nnnorm_eq_spectralRadius, PeriodPair.hasSum_sumInvPow, DirichletCharacter.LFunctionTrivChar_residue_one, hasDerivAt_tan, lintegral_comp_pi_polarCoord_symm, EisensteinSeries.eisensteinSeries_tendstoLocallyUniformlyOn, conformalAt_iff_differentiableAt_or_differentiableAt_comp_conj, rotation_symm, LSeriesHasSum.sum, CompletelyPositiveMap.map_cstarMatrix_nonneg', equivRealProdCLM_symm_apply_im, polarCoord_symm_apply, AnalyticOnNhd.is_constant_or_isOpen, UnitAddTorus.mFourier_single, Real.hasFDerivAt_fourierChar_neg_bilinear_right, summable_bernoulli_fourier, Real.fourier_continuousMultilinearMap_apply, ModularFormClass.differentiableOn_cuspFunction_ball, WeakFEPair.f_modif_aux1, ZMod.differentiable_completedLFunction₀, PeriodPair.periodic_weierstrassP, ModularFormClass.holo, ZMod.toCircle_apply, completedRiemannZeta_residue_one, unitary.norm_sub_one_lt_two_iff, GaussianFourier.integrable_cexp_neg_sum_mul_add, WithCStarModule.pi_norm_sq, hasSum_sinh, NumberField.mixedEmbedding.polarCoord_target_eq_polarCoordReal_target, Circle.arg_exp, MeasureTheory.Lp.toTemperedDistribution_apply, TemperedDistribution.smulLeftCLM_const, SchwartzMap.fourier_fderivCLM_eq, SchwartzMap.fourier_convolution_apply, UpperHalfPlane.sinh_half_dist, hasStrictFDerivAt_log_real, differentiableAt_Gamma, Real.iteratedDeriv_fourierIntegral, UpperHalfPlane.dist_le_iff_le_sinh, TemperedDistribution.smulLeftCLM_sum, NumberField.InfinitePlace.Completion.WithAbs.ratCast_equiv, HurwitzZeta.differentiableAt_cosZeta, hasSum_sin', jacobiTheta₂_fderiv_undef, NumberField.mixedEmbedding.euclidean.finrank, arg_eq_nhds_of_re_neg_of_im_pos, Real.differentiable_fourierChar_neg_bilinear_left, EisensteinSeries.summable_linear_right_add_one_mul_linear_right, gelfandTransform_isometry, Quaternion.coe_ofComplex, betaIntegral_convergent_left, hasSum_one_div_pow_mul_fourier_mul_bernoulliFun, continuousAt_cpow_of_re_pos, TemperedDistribution.instContinuousFourierInv, NumberField.mixedEmbedding.measurableSet_negAt_plusPart, MeasureTheory.SignedMeasure.toComplexMeasure_apply_im, sin_eq_tsum', mellin_differentiableAt_of_isBigO_rpow, one_add_cpow_hasFPowerSeriesOnBall_zero, reCLM_norm, im_eq_zero_iff_isSelfAdjoint, UpperHalfPlane.dist_coe_center_sq, VectorFourier.fourierPowSMulRight_iteratedFDeriv_fourierIntegral, VonNeumannAlgebra.instStarMemClass, ZMod.LFunction_residue_one, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, NormedAlgebra.Complex.nonempty_algEquiv, NumberField.mixedEmbedding.convexBodySum_convex, PeriodPair.mul_ω₁_add_mul_ω₂_mem_lattice, Circle.coe_exp, convex_halfSpace_im_le, riemannZeta_eulerProduct_tprod, MeasureTheory.ComplexMeasure.toComplexMeasure_to_signedMeasure, cpow_eq_nhds, TemperedDistribution.fourier_apply, NumberField.prod_archAbsVal_eq, differentiable_cosh, tendsto_log_nhdsWithin_im_nonneg_of_re_neg_of_im_zero, fourier_add', MeasureTheory.Integrable.fourier_smul, frontier_setOf_le_re_and_im_le, continuousAt_Gamma, EisensteinSeries.eisensteinSeries_SIF_MDifferentiable, BoundedContinuousFunction.charMonoidHom_apply, differentiable_iteratedDeriv_cos, SchwartzMap.coe_apply, riemannZeta_residue_one, ofReal_tsum, MeasureTheory.ComplexMeasure.equivSignedMeasureₗ_apply, StarAlgebra.elemental.continuous_characterSpaceToSpectrum, AddChar.coe_complexBasis, Polynomial.toAddCircle_X_eq_fourier_one, isTheta_deriv_ofReal_cpow_const_atTop, differentiable_cos, CircleIntegrable.out, VonNeumannAlgebra.instSubringClass, LSeries_hasDerivAt, CStarAlgebra.span_nonneg_inter_ball, one_div_one_sub_hasFPowerSeriesOnBall_zero, Real.hasDerivAt_fourierIntegral, UpperHalfPlane.mdifferentiableAt_iff, fourier_add_half_inv_index, PeriodPair.analyticOnNhd_weierstrassPExcept, NumberField.mixedEmbedding.fundamentalCone.smul_mem_iff_mem, NumberField.canonicalEmbedding_eq_basisMatrix_mulVec, integrable_cexp_quadratic, image_exp_Ioc_eq_sphere, HurwitzZeta.completedHurwitzZetaEven_residue_zero, TemperedDistribution.smulLeftCLM_smul, deriv_circleMap_eq_zero_iff, imCLM_apply, HurwitzZeta.tendsto_hurwitzZeta_sub_one_div_nhds_one, Circle.toUnits_apply, NumberField.mixedEmbedding.normAtAllPlaces_mixedSpaceOfRealSpace, fourierCoeffOn.const_smul, CStarAlgebra.toStarModule, PeriodPair.indep, UpperHalfPlane.tanh_half_dist, Real.fourierInv_eq, isConformalMap_complex_linear, SchwartzMap.tsum_eq_tsum_fourierIntegral, Orientation.kahler_rightAngleRotation_right, CFC.monotoneOn_cfcₙ_rpowIntegrand₀₁, MeasureTheory.intervalIntegrable_charFun, arg_eq_nhds_of_re_neg_of_im_neg, hasSum_arctan, fourier_add, MeasureTheory.charFun_eq_integral_innerProbChar, SchwartzMap.instFourierInvSMul, TemperedDistribution.derivCLM_apply_apply, hasDerivAt_exp, HurwitzZeta.hasSum_int_completedCosZeta, TorusIntegrable.function_integrable, hasSum_cosh, frontier_setOf_lt_re, Orientation.norm_kahler, NumberField.mixedEmbedding.disjoint_span_commMap_ker, conj_tsum, isometryOfOrthonormal_symm_apply, IsStarNormal.instIsometricContinuousFunctionalCalculus, ModularForm.coe_trace, integrable_mul_cexp_neg_mul_sq, frontier_setOf_le_im, hasDerivAt_log_sub_logTaylor, GammaIntegral_convergent, isOpenMap_exp, ZMod.dft_eq_fourier, convex_halfSpace_re_gt, AddChar.complexBasis_apply, Real.probChar_apply, CStarAlgebra.instNonnegSpectrumClassComplexUnital, Unitary.argSelfAdjoint_coe, tendsto_euler_sin_prod', WeakDual.CharacterSpace.exists_apply_eq_zero, polarCoord_target, map_isometryOfOrthonormal, hasDerivAt_log, TemperedDistribution.fourierTransformInv_apply, Circle.coe_injective, hasSum_cos, LinearMap.isSymmetric_iff_inner_map_self_real, isHomeomorphicTrivialFiberBundle_im, HurwitzZeta.hasSum_int_completedSinZeta, zeta_nat_eq_tsum_of_gt_one, spectrum.map_polynomial_aeval, Real.fourierInv_eq', UpperHalfPlane.tendsto_comap_im_ofComplex, Circle.coe_zpow, MellinConvergent.cpow_smul, HurwitzZeta.hasSum_nat_hurwitzZetaOdd_of_mem_Icc, Real.fourierIntegral_deriv, NumberField.InfinitePlace.Completion.Rat.norm_infinitePlace_completion, AddChar.expect_apply_eq_ite, reCLM_enorm, UpperHalfPlane.contMDiff_denom, Polynomial.toAddCircle_C_eq_smul_fourier_zero, riemannZeta_eulerProduct_hasProd, VectorFourier.hasFDerivAt_fourierChar_smul, BoundedContinuousFunction.separatesPoints_charPoly, DirichletCharacter.LSeries_eulerProduct, integrable_cexp_quadratic', one_div_sub_sq_sub_one_div_sq_hasFPowerSeriesOnBall_zero, Real.fourierIntegral_real_eq, PeriodPair.lattice_eq_span_range_basis, IsSelfAdjoint.instNonUnitalIsometricContinuousFunctionalCalculus, CStarAlgebra.exists_sum_four_unitary, frontier_reProdIm, Polynomial.Gal.splits_ℚ_ℂ, NumberField.mixedEmbedding.integral_comp_polarCoord_symm, EisensteinSeries.eisensteinSeriesSIF_mdifferentiable, PeriodPair.ω₁_mem_lattice, SchwartzMap.fourier_convolution, log_inv_eq_integral, OnePoint.isZeroAt_iff, UnitAddTorus.span_mFourierLp_closure_eq_top, ZMod.LFunction_dft, nnnorm_eq_one_of_pow_eq_one, PeriodPair.analyticOnNhd_weierstrassP, HurwitzZeta.hasSum_int_completedHurwitzZetaEven, differentiableAt_cos, WeakFEPair.f_modif_aux2, cfcHom_eq_of_isStarNormal, UpperHalfPlane.mdifferentiable_denom_zpow, mellin_cpow_smul, frontier_setOf_im_le, range_exp_mul_I, Circle.coe_div, isUniformEmbedding_equivRealProd, NumberField.mixedEmbedding.commMap_canonical_eq_mixed, Circle.coe_one, Polynomial.fourierCoeff_toAddCircle, hasFPowerSeriesOnBall_ofScalars_mul_add_zero, hasSum_iff, NumberField.mixedEmbedding.norm_negAt, HurwitzZeta.differentiable_completedHurwitzZetaEven₀, VectorFourier.fourierIntegral_fderiv, HurwitzZeta.differentiable_completedHurwitzZetaOdd, WeakFEPair.Λ_residue_zero, ModularFormClass.hasSum_qExpansion, BoundedContinuousFunction.char_add_eq_mul, Real.fourierIntegralInv_eq, isOpenMap_re, WithCStarModule.prod_inner, approx_Gamma_integral_tendsto_Gamma_integral, UpperHalfPlane.continuous_coe, VectorFourier.norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le, deriv_exp, Real.fderiv_fourierChar_neg_bilinear_left_apply, isConformalMap_iff_is_complex_or_conj_linear, PeriodPair.ω₂_mem_lattice, DirichletCharacter.differentiable_LFunctionTrivChar₁, summable_jacobiTheta₂'_term_iff, Real.fourierIntegral_continuousMultilinearMap_apply', Real.fourier_eq', UpperHalfPlane.mdifferentiable_iff, Real.fourierIntegral_iteratedFDeriv, isOpen_re_gt_EReal, NonUnitalCStarAlgebra.toSMulCommClass, WeakFEPair.Λ_residue_k, integrable_cexp_neg_mul_sq, analyticAt_iff_eventually_differentiableAt, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply, Fourier.fourierIntegral_comp_add_right, UpperHalfPlane.isOpen_upperHalfPlaneSet, continuousFunctionalCalculus_map_id, UpperHalfPlane.isEmbedding_coe, NormedAlgebra.Complex.exists_norm_sub_smul_one_eq_zero, HurwitzZeta.differentiable_completedSinZeta, HurwitzZeta.differentiable_hurwitzZetaEven_sub_hurwitzZetaEven, CFC.conjugate_rpow_neg_one_half, ZetaAsymptotics.tendsto_riemannZeta_sub_one_div_nhds_right, NumberField.mixedEmbedding.normAtPlace_mixedSpaceOfRealSpace, NumberField.mixedEmbedding.measurable_polarSpaceCoord_symm, LindemannWeierstrass.hasDerivAt_cexp_mul_sumIDeriv, PeriodPair.derivWeierstrassPExcept_def, continuousAt_ofReal_cpow_const, NumberField.mixedEmbedding.nnnorm_eq_sup_normAtPlace, circleMap_mem_sphere', Circle.argEquiv_apply_coe, LSeries.hasDerivAt_term, UnitDisc.instIsScalarTower_closedBall_closedBall, UpperHalfPlane.mdifferentiableAt_ofComplex, LSeries_eq_mul_integral', CStarAlgebra.span_unitary, Summable.hasSumUniformlyOn_log_one_add, CFC.complex_exp_eq_normedSpace_exp, le_iff_norm_sqrt_mul_rpow, det_conjLIE, WeakFEPair.differentiable_Λ₀, TemperedDistribution.laplacianCLM_apply, continuousAt_gaussian_integral, coeFn_fourierLp, Real.deriv_fourier, CStarAlgebra.exists_sum_four_nonneg, cfcₙ_complex_eq_real, NumberField.mixedEmbedding.disjoint_negAt_plusPart, UnitDisc.coe_circle_smul, ZMod.stdAddChar_apply, DirichletCharacter.continuousOn_neg_logDeriv_LFunctionTrivChar₁, DirichletCharacter.differentiable_completedLFunction, continuousAt_tan, NumberField.mixedEmbedding.volume_fundamentalDomain_stdBasis, PositiveLinearMap.preGNS_norm_sq, HurwitzZeta.differentiableAt_expZeta, NumberField.house_eq_sup', continuous_im, WeakDual.CharacterSpace.instStarHomClass, NonUnitalCommCStarAlgebra.toIsScalarTower, equivRealProdCLM_apply, Circle.argPartialEquiv_apply, MeasureTheory.charFun_eq_integral_probChar, NumberField.mixedEmbedding.convexBodySum_mem, one_div_sub_hasFPowerSeriesOnBall_zero, EulerProduct.exp_tsum_primes_log_eq_tsum, PeriodPair.finrank_lattice, PeriodPair.derivWeierstrassP_add_coe, orderClosedTopology, CStarMatrix.norm_def, HurwitzZeta.differentiableAt_sinZeta, isEquivalent_sin, NumberField.mixedEmbedding.convexBodyLT'_convex, selfAdjoint.expUnitary_coe, TemperedDistribution.smulLeftCLM_apply_apply, summable_jacobiTheta₂_term_iff, conjCLE_coe, NumberField.mixedEmbedding.mem_rat_span_latticeBasis, continuousOn_one_add_mul_inv, Circle.norm_smul, EisensteinSeries.eisensteinSeries_tendstoLocallyUniformly, mellin_comp_mul_left, BoundedContinuousFunction.char_mem_charPoly, MeasureTheory.SignedMeasure.im_toComplexMeasure, differentiableAt_jacobiTheta, NumberField.mixedEmbedding.fundamentalCone.logMap_normAtAllPlaces, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne, rotation, RCLike.complexLinearIsometryEquiv_apply, pi_mul_cot_pi_q_exp, BoundedContinuousFunction.probCharDual_apply, PeriodPair.weierstrassPExcept_add, SchwartzMap.tsum_eq_tsum_fourier, NumberField.mixedEmbedding.normAtAllPlaces_normAtAllPlaces, hasDerivAt_Gamma_nat, IsClosed.reProdIm, CStarMatrix.inner_toCLM_conjTranspose_right, norm_jacobiTheta₂_term_fderiv_le, isometry_intCast, mellin_comp_mul_right, NonUnitalStarAlgHom.instContinuousLinearMapClassComplex, Summable.tendstoUniformlyOn_tsum_nat_log_one_add, CStarMatrix.toCLM_apply_single_apply, BoundedContinuousFunction.char_apply, tendsto_exp_comap_re_atBot_nhdsNE, differentiable_circleMap, HurwitzZeta.tendsto_hurwitzZetaEven_sub_one_div_nhds_one, integrableOn_exp_mul_complex_Ioi, Unitization.cfcₙ_eq_cfc_inr, isClosed_range_intCast, le_iff_norm_sqrt_mul_sqrt_inv, HurwitzZeta.differentiable_completedCosZeta₀, restrictScalars_toSpanSingleton', Polynomial.fourierCoeff_toAddCircle_eq_zero_of_lt_zero, differentiable_iteratedDeriv_cosh, closedEmbedding_intCast, rectangle_eq_convexHull, NumberField.mixedEmbedding.mixedSpaceOfRealSpace_apply, HurwitzZeta.hurwitzZetaEven_residue_one, unitary.spectrum_subset_slitPlane_iff_norm_lt_two, reCLM_apply, closure_setOf_im_lt, NumberField.mixedEmbedding.lintegral_comp_polarSpaceCoord_symm, PeriodPair.differentiableOn_derivWeierstrassPExcept, conjLIE_symm, fourierCoeff_fourier
instRCLike 📖	CompOp	388 math math: TemperedDistribution.lineDerivOpCLM_eq, MeasureTheory.Lp.toTemperedDistributionCLM_apply, UpperHalfPlane.mdifferentiable_num, TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq, hasSum_mellin_pi_mul_sq', IsSelfAdjoint.quasispectrumRestricts, CuspFormClass.holo, MeasureTheory.charFun_eq_fourierIntegral', PeriodPair.hasFPowerSeriesAt_weierstrassPExcept, Real.hasFDerivAt_fourierChar_neg_bilinear_left, AddDissociated.randomisation, Real.fourierCoeff_tsum_comp_add, UnitAddTorus.coe_mFourierBasis, ModularFormClass.qExpansionFormalMultilinearSeries_apply_norm, ModularFormClass.hasFPowerSeries_cuspFunction, ModularFormClass.qExpansionFormalMultilinearSeries_radius, SchwartzMap.inner_fourier_toL2_eq, SchwartzMap.toLp_fourierTransformInv_eq, PeriodPair.coeff_weierstrassPExceptSeries, ModularForm.mul_slash, meromorphic_digamma, PeriodPair.iteratedDeriv_weierstrassPExcept_self, GammaIntegral_eq_mellin, norm_jacobiTheta₂_term_fderiv_ge, integral_comp_pi_polarCoord_symm, one_add_cpow_hasFPowerSeriesAt_zero, BoundedContinuousFunction.char_neg, Unitization.real_cfcₙ_eq_cfc_inr, circleIntegral.integral_sub_inv_of_mem_ball, fourierCoeffOn.const_mul, mellin_div_const, TemperedDistribution.lineDerivOp_fourier_eq, VonNeumannAlgebra.ext_iff, IsConformalMap.is_complex_or_conj_linear, fourierIntegral_gaussian_innerProductSpace', fourier_gaussian_pi', MeasureTheory.charFun_eq_fourierIntegral, TemperedDistribution.smulLeftCLM_compL_smulLeftCLM, PeriodPair.iteratedDeriv_derivWeierstrassPExcept_self, hasStrictFDerivAt_exp_real, ModularForm.prod_slash, UnitAddTorus.mFourierSubalgebra_closure_eq_top, isSelfAdjoint_iff_isStarNormal_and_spectrumRestricts, MeasureTheory.Lp.instFourierInvSMul, differentiableOn_iteratedDerivWithin_cotTerm, ModularForm.prod_slash_sum_weights, HarmonicAt.analyticAt_complex_partial, integral_rpow_mul_exp_neg_rpow, SchwartzMap.integral_fourierInv_smul_eq, PeriodPair.analyticAt_weierstrassPExcept, summableLocallyUniformlyOn_iteratedDerivWithin_cotTerm, SchwartzMap.inner_toL2_toL2_eq, fourier_gaussian_innerProductSpace, SchwartzMap.toLp_fourierInv_eq, TemperedDistribution.smulLeftCLM_neg, UpperHalfPlane.coe_pos_real_smul, Function.HasTemperateGrowth.toTemperedDistribution_apply, LSeries_iteratedDeriv, starConvex_ofReal_slitPlane, analyticOnNhd_univ_iff_differentiable, taylorSeries_eq_on_ball', fourierCoeff_bernoulli_eq, starConvex_one_slitPlane, TemperedDistribution.instLineDerivLeftSMulReal, TemperedDistribution.fourierInv_lineDerivOp_eq, UpperHalfPlane.mdifferentiable_inv_denom, InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_complexPlane, AddChar.sum_apply_eq_ite, integral_comp_polarCoord_symm, SchwartzMap.integral_norm_sq_fourier, UnitAddTorus.mFourierCoeff_toLp, NumberField.mixedEmbedding.fundamentalCone.smul_mem_of_mem, ext_inner_map, TemperedDistribution.instFourierAdd, PeriodPair.hasFPowerSeriesAt_derivWeierstrassPExcept, LSeries_analyticOnNhd, ContinuousLinearMap.instStarOrderedRing, TemperedDistribution.instFourierSMul, convex_halfSpace_re_le, orthonormal_fourier, UpperHalfPlane.contMDiff_coe, CuspForm.holo', Differentiable.hasFPowerSeriesOnBall, BoundedContinuousFunction.mem_charPoly, TemperedDistribution.delta_apply, PeriodPair.analyticOnNhd_derivWeierstrassPExcept, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply_coe, fourierIntegral_gaussian_pi, hasSum_mellin, iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow, DifferentiableOn.contDiffOn, TemperedDistribution.instContinuousFourier, integral_exp_neg_rpow, UpperHalfPlane.contMDiff_inv_denom, SchwartzMap.delta_apply, SchwartzMap.norm_fourier_toL2_eq, norm_cauchyPowerSeries_le, fourier_gaussian_innerProductSpace', hasSum_fourier_series_L2, ProbabilityTheory.iteratedDeriv_complexMGF, convex_halfSpace_im_gt, AddChar.expect_apply_eq_zero_iff_ne_zero, inner_map_polarization', PositiveLinearMap.preGNS_inner_def, SchwartzMap.norm_fourierTransformCLM_toL2_eq, VonNeumannAlgebra.centralizer_centralizer', NumberField.mixedEmbedding.convexBodySumFun_smul, NumberField.mixedEmbedding.logMap_real_smul, AddChar.sum_apply_eq_zero_iff_ne_zero, ProbabilityTheory.analyticAt_complexMGF, HurwitzZeta.hurwitzEvenFEPair_zero_symm, circleIntegral.integral_sub_zpow_of_undef, PeriodPair.weierstrassPExcept_eq_tsum, HasDerivWithinAt.complexToReal_fderiv, TemperedDistribution.fourier_toTemperedDistributionCLM_eq, PeriodPair.meromorphic_derivWeierstrassP, SchwartzMap.convolution_apply, TemperedDistribution.fourierTransformInv_toTemperedDistributionCLM_eq, SchwartzMap.fourierInv_apply_eq, SchwartzMap.toTemperedDistributionCLM_apply_apply, HasDerivAt.complexToReal_fderiv, TemperedDistribution.smulLeftCLM_sub, one_add_cpow_hasFPowerSeriesAt_zero, MeasureTheory.Lp.instFourierSMul, UpperHalfPlane.contMDiff_num, UpperHalfPlane.mdifferentiable_denom, RCLike.sqrt_complex, convex_halfSpace_im_lt, VonNeumannAlgebra.mem_carrier, VonNeumannAlgebra.centralizer_centralizer, eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet, one_div_sub_sq_hasFPowerSeriesOnBall_zero, cfcHom_real_eq_restrict, IsSelfAdjoint.spectrumRestricts, eqOn_iteratedDeriv_cotTerm, one_div_one_sub_pow_hasFPowerSeriesOnBall_zero, UnitAddTorus.orthonormal_mFourier, fourierCoeff_toLp, AddChar.card_eq, coe_fourierBasis, ModularFormClass.qExpansion_coeff, hasSum_sq_fourierCoeffOn, inr_comp_cfcₙHom_eq_cfcₙAux, SpectrumRestricts.real_iff, torusIntegral_const_mul, integral_exp_neg_mul_rpow, hasSum_mellin_pi_mul, le_radius_cauchyPowerSeries, hasMellin_one_Ioc, QuasispectrumRestricts.real_iff, TemperedDistribution.instLineDerivSMulReal, MeasureTheory.Measure.toTemperedDistribution_apply, analyticOn_iff_differentiableOn, TemperedDistribution.fourier_lineDerivOp_eq, TemperedDistribution.fourier_delta_zero, PeriodPair.order_weierstrassP, MeromorphicNFOn.Gamma, iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow, NumberField.mixedEmbedding.norm_smul, PositiveLinearMap.gnsStarAlgHom_apply, lintegral_comp_polarCoord_symm, LinearMap.isPositive_iff_complex, UnitAddTorus.instContinuousSMulComplexSubtypeAEEqFunVolumeMemAddSubgroupLp, TemperedDistribution.lineDerivOp_toTemperedDistributionCLM_eq, isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts, UnitAddTorus.hasSum_mFourier_series_L2, TemperedDistribution.laplacian_eq_sum, TemperedDistribution.instContinuousLineDeriv, volume_preserving_equiv_real_prod, one_div_sub_pow_hasFPowerSeriesOnBall_zero, HadamardThreeLines.diffContOnCl_interpStrip, hasFPowerSeriesOn_cauchy_integral, UpperHalfPlane.contMDiff_denom_zpow, circleIntegral_div_sub_of_differentiable_on_off_countable, convex_halfSpace_re_ge, DifferentiableOn.hasFPowerSeriesOnBall, analyticOn_univ_iff_differentiable, fourierIntegral_gaussian_innerProductSpace, Differentiable.contDiff, HurwitzZeta.hurwitzOddFEPair_f₀, convex_halfSpace_im_ge, cot_pi_mul_contDiffWithinAt, convex_halfSpace_re_lt, TemperedDistribution.smulLeftCLM_add, PeriodPair.coeff_weierstrassPSeries, locallyFinsuppWithin.logCounting_divisor, HurwitzZeta.hurwitzOddFEPair_ε, Unitization.nnreal_cfcₙ_eq_cfc_inr, sqrt_map, TemperedDistribution.fourierTransform_apply, isConformalMap_complex_linear_conj, hasSum_mellin_pi_mul₀, cfcₙHom_real_eq_restrict, PeriodPair.hasFPowerSeriesOnBall_weierstrassP, NumberField.canonicalEmbedding.mem_rat_span_latticeBasis, harmonic_is_realOfHolomorphic, PeriodPair.weierstrassPSeries_hasSum, span_fourierLp_closure_eq_top, circleIntegral.integral_sub_zpow_of_ne, LindemannWeierstrass.integral_exp_mul_eval, LSeries.iteratedDeriv_alternating, SchwartzMap.inner_fourierTransformCLM_toL2_eq, inner_map_self_eq_zero, circleIntegral.integral_smul_const, InnerProductSpace.laplacian_eq_iteratedFDeriv_complexPlane, SchwartzMap.integral_fourier_mul_eq, volume_preserving_equiv_pi, PeriodPair.hasFPowerSeriesOnBall_derivWeierstrassPExcept, Polynomial.fourierCoeff_toAddCircle_natCast, fourierCoeffOn_of_hasDerivAt_Ioo, PeriodPair.analyticOnNhd_derivWeierstrassP, NumberField.mixedEmbedding.convexBodyLT_convex, hasFPowerSeriesOnBall_cuspFunction, tsum_sq_fourierCoeffOn, ModularFormClass.qExpansion_coeff_eq_circleIntegral, one_div_one_sub_cpow_hasFPowerSeriesOnBall_zero, NormedAlgebra.Real.nonempty_algEquiv_or, PeriodPair.meromorphic_weierstrassP, PeriodPair.analyticAt_derivWeierstrassPExcept, TemperedDistribution.instFourierInvSMul, ContinuousLinearMap.isPositive_iff_complex, HurwitzZeta.hurwitzOddFEPair_g₀, SchwartzMap.toLp_fourierTransform_eq, TemperedDistribution.instFourierInvAdd, MeasureTheory.Lp.fourierInv_toTemperedDistribution_eq, UnitAddTorus.hasSum_prod_mFourierCoeff, circleIntegral.circleIntegral_congr_codiscreteWithin, BoundedContinuousFunction.star_mem_range_charAlgHom, TemperedDistribution.fourierInv_apply, HurwitzZeta.hurwitzOddFEPair_f, fourierCoeff.const_mul, TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq, one_add_cpow_hasFPowerSeriesOnBall_zero, SchwartzMap.fderivCLM_fourier_eq, TemperedDistribution.instLineDerivAdd, NumberField.mixedEmbedding.logMap_real, MeasureTheory.Lp.inner_fourier_eq, TemperedDistribution.instLineDerivSMulComplex, LSeries_analyticOn, log_eq_integral, one_div_one_sub_sq_hasFPowerSeriesOnBall_zero, SchwartzMap.integral_fourierInv_mul_eq, TemperedDistribution.laplacian_toTemperedDistributionCLM_eq, VonNeumannAlgebra.coe_toStarSubalgebra, mdifferentiable_jacobiTheta, PeriodPair.hasFPowerSeriesOnBall_weierstrassPExcept, NumberField.mixedEmbedding.normAtPlace_smul, ProbabilityTheory.hasDerivAt_iteratedDeriv_complexMGF, SchwartzMap.integral_fourier_smul_eq, HurwitzZeta.hurwitzOddFEPair_k, UpperHalfPlane.contMDiffAt_ofComplex, fourierSubalgebra_closure_eq_top, ModularForm.prod_fintype_slash, RCLike.ofReal_eq_complex_ofReal, ModularForm.holo', Real.nonempty_algEquiv_or, starConvex_slitPlane, ProbabilityTheory.analyticOn_complexMGF, integral_rpow_mul_exp_neg_mul_rpow, RCLike.im_to_complex, AddChar.doubleDualEquiv_symm_doubleDualEmb_apply, iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum, inner_map_polarization, RCLike.re_eq_complex_re, TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq, DifferentiableOn.analyticOnNhd, hasSum_sq_fourierCoeff, UpperHalfPlane.contMDiffAt_iff, Orientation.kahler_apply_apply, UpperHalfPlane.instIsManifoldComplexModelWithCornersSelfTopWithTopENat, taylorSeries_eq_on_eball', VonNeumannAlgebra.mem_commutant_iff, UnitAddTorus.mFourierBasis_repr, Function.Periodic.contDiff_qParam, analyticOnNhd_iff_differentiableOn, MeasureTheory.Lp.ker_toTemperedDistributionCLM_eq_bot, MeasureTheory.Lp.toTemperedDistribution_toLp_eq, fourierBasis_repr, analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt, TemperedDistribution.laplacian_apply_apply, TemperedDistribution.smulLeftCLM_smulLeftCLM_apply, UpperHalfPlane.mdifferentiable_coe, PeriodPair.weierstrassPExceptSeries_hasSum, RCLike.toContinuousLinearMap_complexLinearIsometryEquiv, ModularFormClass.analyticAt_cuspFunction_zero, TemperedDistribution.lineDerivOp_apply_apply, HadamardThreeLines.diffContOnCl_invInterpStrip, Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv, UnitAddTorus.hasSum_sq_mFourierCoeff, TemperedDistribution.lineDerivOp_fourierInv_eq, HurwitzZeta.hurwitzOddFEPair_g, VonNeumannAlgebra.coe_commutant, circleTransformDeriv_bound, hasFPowerSeriesOnBall_of_differentiable_off_countable, lintegral_comp_pi_polarCoord_symm, analyticAt_clog, Real.hasFDerivAt_fourierChar_neg_bilinear_right, RCLike.im_eq_complex_im, SchwartzMap.integral_inner_fourier_fourier, ModularFormClass.holo, circleIntegral.integral_sub_center_inv, MeasureTheory.Lp.toTemperedDistribution_apply, TemperedDistribution.smulLeftCLM_const, SchwartzMap.fourier_fderivCLM_eq, SchwartzMap.fourier_convolution_apply, hasStrictFDerivAt_log_real, TemperedDistribution.smulLeftCLM_sum, Quaternion.coe_ofComplex, fourierCoeff_liftIoc_eq, TemperedDistribution.instContinuousFourierInv, one_add_cpow_hasFPowerSeriesOnBall_zero, VonNeumannAlgebra.instStarMemClass, NumberField.mixedEmbedding.convexBodySum_convex, convex_halfSpace_im_le, TemperedDistribution.fourier_apply, RCLike.normSq_to_complex, hasMellin_cpow_Ioc, EisensteinSeries.eisensteinSeries_SIF_MDifferentiable, tsum_sq_fourierCoeff, VectorFourier.integral_fourierIntegral_smul_eq_flip, SchwartzMap.coe_apply, DifferentiableOn.analyticAt, VonNeumannAlgebra.instSubringClass, one_div_one_sub_hasFPowerSeriesOnBall_zero, UpperHalfPlane.mdifferentiableAt_iff, fourierCoeffOn_of_hasDerivAt, PeriodPair.analyticOnNhd_weierstrassPExcept, NumberField.mixedEmbedding.fundamentalCone.smul_mem_iff_mem, TemperedDistribution.smulLeftCLM_smul, ArithmeticFunction.iteratedDeriv_LSeries_alternating, isConformalMap_complex_linear, SchwartzMap.tsum_eq_tsum_fourierIntegral, TemperedDistribution.derivCLM_apply_apply, taylorSeries_eq_of_entire', Meromorphic.Gamma, HasStrictDerivAt.complexToReal_fderiv, convex_halfSpace_re_gt, ProbabilityTheory.analyticOnNhd_complexMGF, TemperedDistribution.fourierTransformInv_apply, LinearMap.isSymmetric_iff_inner_map_self_real, ModularFormClass.qExpansionFormalMultilinearSeries_coeff, UpperHalfPlane.contMDiff_smul, eqOn_iteratedDerivWithin_cotTerm_integerComplement, AddChar.expect_apply_eq_ite, UpperHalfPlane.contMDiff_denom, BoundedContinuousFunction.separatesPoints_charPoly, one_div_sub_sq_sub_one_div_sq_hasFPowerSeriesOnBall_zero, RCLike.re_to_complex, EisensteinSeries.eisensteinSeriesSIF_mdifferentiable, log_inv_eq_integral, UnitAddTorus.span_mFourierLp_closure_eq_top, PeriodPair.analyticOnNhd_weierstrassP, UpperHalfPlane.mdifferentiable_denom_zpow, MeromorphicOn.Gamma, Polynomial.fourierCoeff_toAddCircle, hasFPowerSeriesOnBall_ofScalars_mul_add_zero, MeasureTheory.Lp.fourier_toTemperedDistribution_eq, SchwartzMap.toLp_fourier_eq, isConformalMap_iff_is_complex_or_conj_linear, UpperHalfPlane.mdifferentiable_iff, analyticAt_iff_eventually_differentiableAt, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply, fourierCoeffOn_of_hasDeriv_right, LindemannWeierstrass.hasDerivAt_cexp_mul_sumIDeriv, UpperHalfPlane.mdifferentiableAt_ofComplex, fourier_gaussian_pi, Real.fourier_smul_convolution_eq, TemperedDistribution.laplacianCLM_apply, taylorSeries_eq_on_emetric_ball', fourierCoeff_liftIco_eq, circleIntegral.integral_const_mul, MeasureTheory.Lp.toTemperedDistribution_smul_eq, Differentiable.analyticAt, one_div_sub_hasFPowerSeriesOnBall_zero, fourierIntegral_gaussian_pi', RCLike.I_to_complex, NumberField.mixedEmbedding.convexBodyLT'_convex, TemperedDistribution.smulLeftCLM_apply_apply, NumberField.mixedEmbedding.mem_rat_span_latticeBasis, hasSum_mellin_pi_mul_sq, continuousOn_one_add_mul_inv, BoundedContinuousFunction.char_mem_charPoly, SchwartzMap.tsum_eq_tsum_fourier, norm_jacobiTheta₂_term_fderiv_le, UpperHalfPlane.mdifferentiable_smul, Polynomial.fourierCoeff_toAddCircle_eq_zero_of_lt_zero, DifferentiableOn.analyticOn, fourierCoeff_fourier
ofRealCLM 📖	CompOp	7 math math: Real.hasFDerivAt_fourierChar_neg_bilinear_left, ofRealCLM_coe, ofRealCLM_norm, ofRealCLM_nnnorm, ofRealCLM_apply, ofRealCLM_enorm, Real.hasFDerivAt_fourierChar_neg_bilinear_right
ofRealLI 📖	CompOp	1 math math: ofRealLI_apply
reCLM 📖	CompOp	18 math math: restrictScalars_one_smulRight', IsSelfAdjoint.quasispectrumRestricts, HasDerivWithinAt.complexToReal_fderiv', isSelfAdjoint_iff_isStarNormal_and_spectrumRestricts, reCLM_nnnorm, reCLM_coe, HasDerivAt.complexToReal_fderiv', cfcHom_real_eq_restrict, IsSelfAdjoint.spectrumRestricts, SpectrumRestricts.real_iff, QuasispectrumRestricts.real_iff, isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts, HasStrictDerivAt.complexToReal_fderiv', cfcₙHom_real_eq_restrict, reCLM_norm, reCLM_enorm, restrictScalars_toSpanSingleton', reCLM_apply
slitPlane 📖	CompOp	24 math math: subset_slitPlane_iff_of_subset_sphere, continuousOn_arg, isOpen_slitPlane, starConvex_ofReal_slitPlane, starConvex_one_slitPlane, mem_slitPlane_iff_arg, ofNat_mem_slitPlane, natCast_mem_slitPlane, slitPlane_eq_union, Unitary.spectrum_subset_slitPlane_iff_norm_lt_two, mem_slitPlane_of_norm_lt_one, ball_one_subset_slitPlane, polarCoord_source, ofReal_mem_slitPlane, mem_slitPlane_iff, exp_mem_slitPlane, compl_Iic_zero, starConvex_slitPlane, neg_ofReal_mem_slitPlane, zero_notMem_slitPlane, one_mem_slitPlane, mem_slitPlane_or_neg_mem_slitPlane, mem_slitPlane_iff_not_le_zero, unitary.spectrum_subset_slitPlane_iff_norm_lt_two

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antilipschitz_equivRealProd 📖	mathematical	—	AntilipschitzWith Complex Real EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace instNormedField Prod.pseudoEMetricSpaceMax Real.metricSpace DFunLike.coe OrderIso NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal instFunLikeOrderIso NNReal.sqrt instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instSemiringNNReal Nat.instAtLeastTwoHAddOfNat Equiv EquivLike.toFunLike Equiv.instEquivLike equivRealProd	—	AddMonoidHomClass.antilipschitz_of_bound RingHomInvPair.ids DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Nat.instAtLeastTwoHAddOfNat Real.coe_sqrt norm_le_sqrt_two_mul_max
ball_one_subset_slitPlane 📖	mathematical	—	Set Complex Set.instHasSubset Metric.ball SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField instOne Real Real.instOne slitPlane	—	neg_lt_of_abs_lt IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add LE.le.trans_lt abs_re_le_norm lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le
closedEmbedding_intCast 📖	mathematical	—	Topology.IsClosedEmbedding Complex instTopologicalSpaceInt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField instIntCast	—	Isometry.isClosedEmbedding DiscreteUniformity.instCompleteSpace DiscreteUniformity.inst isometry_intCast
compl_Iic_zero 📖	mathematical	—	Compl.compl Set Complex Set.instCompl Set.Iic PartialOrder.toPreorder partialOrder instZero slitPlane	—	Set.ext mem_slitPlane_iff_not_le_zero
conjCLE_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedSpace.complexToReal NormedField.toNormedSpace EquivLike.toFunLike ContinuousLinearEquiv.equivLike conjCLE RingHom CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing	—	RingHomInvPair.ids
conjCLE_coe 📖	mathematical	—	ContinuousLinearEquiv.toLinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedSpace.complexToReal NormedField.toNormedSpace conjCLE AlgEquiv.toLinearEquiv Real.instCommSemiring instSemiring Algebra.complexToReal Algebra.id instCommSemiring conjAe	—	RingHomInvPair.ids
conjLIE_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField NormedSpace.toModule Real.normedField NormedSpace.complexToReal NormedField.toNormedSpace EquivLike.toFunLike LinearIsometryEquiv.instEquivLike conjLIE RingHom CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing	—	RingHomInvPair.ids
conjLIE_symm 📖	mathematical	—	LinearIsometryEquiv.symm Real Complex Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField NormedSpace.toModule Real.normedField NormedSpace.complexToReal NormedField.toNormedSpace conjLIE	—	RingHomInvPair.ids
conj_mul' 📖	mathematical	—	Complex instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring ofReal Norm.norm instNorm	—	RCLike.conj_mul
conj_tsum 📖	mathematical	—	DFunLike.coe RingHom Complex Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing tsum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup	—	RCLike.conj_tsum
continuous_conj 📖	mathematical	—	Continuous Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing	—	ContinuousStar.continuous_star instContinuousStar
continuous_im 📖	mathematical	—	Continuous Complex Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Real.pseudoMetricSpace im	—	ContinuousLinearMap.continuous
continuous_normSq 📖	mathematical	—	Continuous Complex Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Real.pseudoMetricSpace DFunLike.coe MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instSemiring Real.semiring MonoidWithZeroHom.funLike normSq	—	Continuous.pow IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuous_norm
continuous_ofReal 📖	mathematical	—	Continuous Real Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ofReal	—	LinearIsometry.continuous
continuous_re 📖	mathematical	—	Continuous Complex Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Real.pseudoMetricSpace re	—	ContinuousLinearMap.continuous
dist_conj_comm 📖	mathematical	—	Dist.dist Complex PseudoMetricSpace.toDist SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing	—	dist_conj_conj conj_conj
dist_conj_conj 📖	mathematical	—	Dist.dist Complex PseudoMetricSpace.toDist SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing	—	Isometry.dist_eq isometry_conj
eq_coe_norm_of_nonneg 📖	mathematical	Complex Preorder.toLE PartialOrder.toPreorder partialOrder instZero	ofReal Norm.norm instNorm	—	CanLift.prf canLift norm_real Real.norm_of_nonneg
equivRealProdCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup instTopologicalSpaceProd Real.pseudoMetricSpace Prod.instAddCommMonoid Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedSpace.complexToReal NormedField.toNormedSpace Prod.instModule Real.normedCommRing EquivLike.toFunLike ContinuousLinearEquiv.equivLike equivRealProdCLM re im	—	RingHomInvPair.ids
equivRealProdCLM_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Prod.instAddCommMonoid Real.instAddCommMonoid Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup Prod.instModule NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace NormedSpace.complexToReal EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm equivRealProdCLM instAdd ofReal instMul I	—	equivRealProd_symm_apply
equivRealProdCLM_symm_apply_im 📖	mathematical	—	im DFunLike.coe ContinuousLinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Prod.instAddCommMonoid Real.instAddCommMonoid Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup Prod.instModule NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace NormedSpace.complexToReal EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm equivRealProdCLM	—	RingHomInvPair.ids
equivRealProdCLM_symm_apply_re 📖	mathematical	—	re DFunLike.coe ContinuousLinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Prod.instAddCommMonoid Real.instAddCommMonoid Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup Prod.instModule NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace NormedSpace.complexToReal EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm equivRealProdCLM	—	RingHomInvPair.ids
equivRealProd_apply_le 📖	mathematical	—	Real Real.instLE Norm.norm Prod.toNorm Real.norm DFunLike.coe Equiv Complex EquivLike.toFunLike Equiv.instEquivLike equivRealProd instNorm	—	—
equivRealProd_apply_le' 📖	mathematical	—	Real Real.instLE Norm.norm Prod.toNorm Real.norm DFunLike.coe Equiv Complex EquivLike.toFunLike Equiv.instEquivLike equivRealProd Real.instMul Real.instOne instNorm	—	one_mul equivRealProd_apply_le
exists_norm_eq_mul_self 📖	mathematical	—	Norm.norm Complex instNorm Real Real.instOne ofReal instMul	—	RCLike.exists_norm_eq_mul_self
exists_norm_mul_eq_self 📖	mathematical	—	Norm.norm Complex instNorm Real Real.instOne instMul ofReal	—	RCLike.exists_norm_mul_eq_self
hasSum_conj 📖	mathematical	—	HasSum Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing	—	RCLike.hasSum_conj
hasSum_conj' 📖	mathematical	—	HasSum Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing	—	RCLike.hasSum_conj'
hasSum_iff 📖	mathematical	—	HasSum Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup Real Real.instAddCommMonoid Real.pseudoMetricSpace re im	—	RCLike.hasSum_iff
hasSum_im 📖	mathematical	HasSum Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup	Real Real.instAddCommMonoid Real.pseudoMetricSpace im	—	RCLike.hasSum_im
hasSum_ofReal 📖	mathematical	—	HasSum Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup ofReal Real Real.instAddCommMonoid Real.pseudoMetricSpace	—	RCLike.hasSum_ofReal
hasSum_re 📖	mathematical	HasSum Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup	Real Real.instAddCommMonoid Real.pseudoMetricSpace re	—	RCLike.hasSum_re
imCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup Real.pseudoMetricSpace Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedSpace.complexToReal NormedField.toNormedSpace Real.normedCommRing ContinuousLinearMap.funLike imCLM im	—	—
imCLM_coe 📖	mathematical	—	ContinuousLinearMap.toLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup Real.pseudoMetricSpace Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedSpace.complexToReal NormedField.toNormedSpace Real.normedCommRing imCLM imLm	—	—
im_eq_zero_iff_isSelfAdjoint 📖	mathematical	—	im Real Real.instZero IsSelfAdjoint Complex InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing instNormedField StarRing.toStarAddMonoid instStarRing	—	RCLike.im_eq_complex_im RCLike.im_eq_zero_iff_isSelfAdjoint
im_tsum 📖	mathematical	Summable Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup	im tsum Real Real.instAddCommMonoid Real.pseudoMetricSpace	—	RCLike.im_tsum
instCompleteSpace 📖	mathematical	—	CompleteSpace Complex PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField	—	completeSpace_congr isUniformEmbedding_equivRealProd CompleteSpace.prod Real.instCompleteSpace
instContinuousStar 📖	mathematical	—	ContinuousStar Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing StarRing.toStarAddMonoid instStarRing	—	LinearIsometryEquiv.continuous RingHomInvPair.ids
instProperSpace 📖	mathematical	—	ProperSpace Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField	—	LipschitzWith.properSpace prod_properSpace instProperSpaceReal RingHomInvPair.ids Homeomorph.isProperMap lipschitz_equivRealProd
instT2Space 📖	mathematical	—	T2Space Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField	—	TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
inv_eq_conj 📖	mathematical	Norm.norm Complex instNorm Real Real.instOne	instInv DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing	—	RCLike.inv_eq_conj
isClosed_range_intCast 📖	mathematical	—	IsClosed Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Set.range instIntCast	—	Topology.IsClosedEmbedding.isClosed_range closedEmbedding_intCast
isOpen_compl_range_intCast 📖	mathematical	—	IsOpen Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Compl.compl Set Set.instCompl Set.range instIntCast	—	IsClosed.isOpen_compl isClosed_range_intCast
isOpen_slitPlane 📖	mathematical	—	IsOpen Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField slitPlane	—	IsOpen.union isOpen_lt RCLike.instOrderClosedTopology continuous_const continuous_re isOpen_ne_fun TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace continuous_im
isUniformEmbedding_equivRealProd 📖	mathematical	—	IsUniformEmbedding Complex Real PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField instUniformSpaceProd Real.pseudoMetricSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike equivRealProd	—	AntilipschitzWith.isUniformEmbedding Nat.instAtLeastTwoHAddOfNat antilipschitz_equivRealProd LipschitzWith.uniformContinuous lipschitz_equivRealProd
isUniformEmbedding_ofReal 📖	mathematical	—	IsUniformEmbedding Real Complex PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ofReal	—	Isometry.isUniformEmbedding LinearIsometry.isometry
isometry_conj 📖	mathematical	—	Isometry Complex EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace instNormedField DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing	—	LinearIsometryEquiv.isometry RingHomInvPair.ids
isometry_intCast 📖	mathematical	—	Isometry Complex EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Int.instMetricSpace NormedField.toMetricSpace instNormedField instIntCast	—	Isometry.of_dist_eq Isometry.dist_eq isometry_ofReal
isometry_ofReal 📖	mathematical	—	Isometry Real Complex EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Real.metricSpace NormedField.toMetricSpace instNormedField ofReal	—	LinearIsometry.isometry
le_of_eq_sum_of_eq_sum_norm 📖	—	Real Real.instLE Real.instZero ofReal Finset.sum Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup Norm.norm instNorm	—	—	norm_of_nonneg norm_sum_le
lipschitz_equivRealProd 📖	mathematical	—	LipschitzWith Complex Real EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace instNormedField Prod.pseudoEMetricSpaceMax Real.metricSpace NNReal instOneNNReal DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike equivRealProd	—	RingHomInvPair.ids Real.toNNReal_one AddMonoidHomClass.lipschitz_of_bound DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass equivRealProd_apply_le'
mem_slitPlane_iff 📖	mathematical	—	Complex Set Set.instMembership slitPlane Real Real.instLT Real.instZero re	—	Set.mem_setOf
mem_slitPlane_iff_not_le_zero 📖	mathematical	—	Complex Set Set.instMembership slitPlane Preorder.toLE PartialOrder.toPreorder partialOrder instZero	—	mem_slitPlane_iff not_le_zero_iff
mem_slitPlane_of_norm_lt_one 📖	mathematical	Real Real.instLT Norm.norm Complex instNorm Real.instOne	Set Set.instMembership slitPlane instAdd instOne	—	ball_one_subset_slitPlane dist_self_add_left
mem_slitPlane_or_neg_mem_slitPlane 📖	mathematical	—	Complex Set Set.instMembership slitPlane instNeg	—	mem_slitPlane_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Tactic.Push.not_and_eq ext_iff le_antisymm
mul_conj' 📖	mathematical	—	Complex instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring ofReal Norm.norm instNorm	—	RCLike.mul_conj
natCast_mem_slitPlane 📖	mathematical	—	Complex Set Set.instMembership slitPlane instNatCast	—	Real.instIsOrderedRing Real.instNontrivial Nat.instCanonicallyOrderedAdd ofReal_mem_slitPlane
neg_ofReal_mem_slitPlane 📖	mathematical	—	Complex Set Set.instMembership slitPlane instNeg ofReal Real Real.instLT Real.instZero	—	ofReal_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid ofReal_mem_slitPlane
nndist_conj_comm 📖	mathematical	—	NNDist.nndist Complex PseudoMetricSpace.toNNDist SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing	—	dist_conj_comm
nndist_conj_conj 📖	mathematical	—	NNDist.nndist Complex PseudoMetricSpace.toNNDist SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing	—	Isometry.nndist_eq isometry_conj
nnnorm_eq_one_of_pow_eq_one 📖	mathematical	Complex Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring instOne	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField NNReal instOneNNReal	—	pow_left_inj₀ LinearOrderedCommMonoidWithZero.toPosMulStrictMono IsOrderedRing.toMulPosMono NNReal.instIsOrderedRing zero_le' nnnorm_pow NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass nnnorm_one one_pow
nnnorm_intCast 📖	mathematical	—	NNNorm.nnnorm Complex SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField instIntCast Int.instNormedCommRing	—	NNReal.eq norm_intCast
norm_eq_one_of_pow_eq_one 📖	mathematical	Complex Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring instOne	Norm.norm instNorm Real Real.instOne	—	nnnorm_eq_one_of_pow_eq_one
norm_of_nonneg' 📖	mathematical	Complex Preorder.toLE PartialOrder.toPreorder partialOrder instZero	ofReal Norm.norm instNorm	—	RCLike.ofReal_eq_complex_ofReal RCLike.norm_of_nonneg'
ofNat_mem_slitPlane 📖	mathematical	—	Complex Set Set.instMembership slitPlane	—	natCast_mem_slitPlane Nat.AtLeastTwo.toNeZero
ofRealCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instAddCommMonoid Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace NormedSpace.complexToReal ContinuousLinearMap.funLike ofRealCLM ofReal	—	—
ofRealCLM_coe 📖	mathematical	—	ContinuousLinearMap.toLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instAddCommMonoid Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace NormedSpace.complexToReal ofRealCLM AlgHom.toLinearMap Real.instCommSemiring instSemiring Algebra.id Algebra.complexToReal instCommSemiring ofRealAm	—	—
ofRealLI_apply 📖	mathematical	—	DFunLike.coe LinearIsometry Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedCommRing instNormedField NormedSpace.toModule Real.normedField NormedField.toNormedSpace NormedSpace.complexToReal LinearIsometry.instFunLike ofRealLI ofReal	—	—
ofReal_eq_re_of_isSelfAdjoint 📖	mathematical	IsSelfAdjoint Complex InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing instNormedField StarRing.toStarAddMonoid instStarRing	re ofReal	—	RCLike.re_eq_complex_re RCLike.ofReal_eq_re_of_isSelfAdjoint
ofReal_mem_slitPlane 📖	mathematical	—	Complex Set Set.instMembership slitPlane ofReal Real Real.instLT Real.instZero	—	—
ofReal_tsum 📖	mathematical	—	ofReal tsum Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Complex ESeminormedAddCommMonoid.toAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup	—	RCLike.ofReal_tsum
one_mem_slitPlane 📖	mathematical	—	Complex Set Set.instMembership slitPlane instOne	—	ofReal_mem_slitPlane one_pos Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
orderClosedTopology 📖	mathematical	—	OrderClosedTopology Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField PartialOrder.toPreorder partialOrder	—	IsClosed.inter isClosed_le RCLike.instOrderClosedTopology Continuous.comp' continuous_re continuous_fst continuous_snd isClosed_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace continuous_im
reCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup Real.pseudoMetricSpace Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedSpace.complexToReal NormedField.toNormedSpace Real.normedCommRing ContinuousLinearMap.funLike reCLM re	—	—
reCLM_coe 📖	mathematical	—	ContinuousLinearMap.toLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup Real.pseudoMetricSpace Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedSpace.complexToReal NormedField.toNormedSpace Real.normedCommRing reCLM reLm	—	—
re_eq_ofReal_of_isSelfAdjoint 📖	mathematical	IsSelfAdjoint Complex InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing instNormedField StarRing.toStarAddMonoid instStarRing	re ofReal	—	RCLike.re_eq_complex_re RCLike.re_eq_ofReal_of_isSelfAdjoint
re_le_re 📖	mathematical	Complex Preorder.toLE PartialOrder.toPreorder partialOrder	Real Real.instLE re	—	RCLike.le_iff_re_im
re_nonneg_iff_nonneg 📖	mathematical	IsSelfAdjoint Complex InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing instNormedField StarRing.toStarAddMonoid instStarRing	Real Real.instLE Real.instZero re Preorder.toLE PartialOrder.toPreorder partialOrder instZero	—	RCLike.re_eq_complex_re RCLike.re_nonneg_of_nonneg
re_tsum 📖	mathematical	Summable Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup	re tsum Real Real.instAddCommMonoid Real.pseudoMetricSpace	—	RCLike.re_tsum
restrictScalars_one_smulRight 📖	mathematical	—	ContinuousLinearMap.restrictScalars Complex Real instSemiring Real.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField NormedSpace.complexToReal NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup instModuleSelf LinearMap.IsScalarTower.compatibleSMul' SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsScalarTower.right Semifield.toCommSemiring Field.toSemifield NormedField.toField Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra instNormedAlgebraOfReal RCLike.toNormedAlgebra Real.instRCLike ContinuousLinearMap.toSpanSingleton ContinuousMul.to_continuousSMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap RingHom.id ContinuousLinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instRing SeminormedAddCommGroup.to_isUniformAddGroup NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ContinuousLinearMap.one	—	restrictScalars_toSpanSingleton
restrictScalars_one_smulRight' 📖	mathematical	—	ContinuousLinearMap.restrictScalars Complex Real instSemiring Real.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField NormedSpace.complexToReal NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.IsScalarTower.compatibleSMul' SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsScalarTower.complexToReal addCommGroup IsScalarTower.left DistribMulAction.toMulAction ContinuousLinearMap.toSpanSingleton IsBoundedSMul.continuousSMul instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul ContinuousLinearMap RingHom.id ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup ContinuousLinearMap.add IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.smulRight Real.normedCommRing Real.pseudoMetricSpace Real.instZero reCLM ContinuousLinearMap.instSMul SMulCommClass.complexToReal smulCommClass_self CommRing.toCommMonoid commRing CommMonoid.toMonoid Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul I imCLM	—	restrictScalars_toSpanSingleton'
restrictScalars_toSpanSingleton 📖	mathematical	—	ContinuousLinearMap.restrictScalars Complex Real instSemiring Real.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField NormedSpace.complexToReal NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup instModuleSelf LinearMap.IsScalarTower.compatibleSMul' SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsScalarTower.right Semifield.toCommSemiring Field.toSemifield NormedField.toField Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra instNormedAlgebraOfReal RCLike.toNormedAlgebra Real.instRCLike ContinuousLinearMap.toSpanSingleton ContinuousMul.to_continuousSMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap RingHom.id ContinuousLinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instRing SeminormedAddCommGroup.to_isUniformAddGroup NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ContinuousLinearMap.one	—	ContinuousLinearMap.ext LinearMap.IsScalarTower.compatibleSMul' IsScalarTower.right ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup mul_comm
restrictScalars_toSpanSingleton' 📖	mathematical	—	ContinuousLinearMap.restrictScalars Complex Real instSemiring Real.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField NormedSpace.complexToReal NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.IsScalarTower.compatibleSMul' SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsScalarTower.complexToReal addCommGroup IsScalarTower.left DistribMulAction.toMulAction ContinuousLinearMap.toSpanSingleton IsBoundedSMul.continuousSMul instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul ContinuousLinearMap RingHom.id ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup ContinuousLinearMap.add IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.smulRight Real.normedCommRing Real.pseudoMetricSpace Real.instZero reCLM ContinuousLinearMap.instSMul SMulCommClass.complexToReal smulCommClass_self CommRing.toCommMonoid commRing CommMonoid.toMonoid Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul I imCLM	—	ContinuousLinearMap.ext LinearMap.IsScalarTower.compatibleSMul' IsScalarTower.complexToReal IsScalarTower.left IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup SMulCommClass.complexToReal smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul mk_eq_add_mul_I map_add SemilinearMapClass.toAddHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass SemigroupAction.mul_smul zero_smul smul_zero add_zero MulZeroClass.mul_zero mul_one sub_self SMulCommClass.smul_comm IsScalarTower.to_smulCommClass' zero_add
ringHom_eq_id_or_conj_of_continuous 📖	mathematical	Continuous Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField DFunLike.coe RingHom Semiring.toNonAssocSemiring instSemiring RingHom.instFunLike	RingHom.id starRingEnd instCommSemiring instStarRing	—	map_real_smul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul instT2Space DistribMulActionSemiHomClass.toAddMonoidHomClass instCharZero SemilinearMapClass.distribMulActionSemiHomClass RingHomClass.toLinearMapClassNNRat RingHom.instRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass real_algHom_eq_id_or_conj
ringHom_eq_ofReal_of_continuous 📖	mathematical	Continuous Real Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField DFunLike.coe RingHom Semiring.toNonAssocSemiring Real.semiring instSemiring RingHom.instFunLike	ofRealHom	—	map_real_smul ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul instT2Space DistribMulActionSemiHomClass.toAddMonoidHomClass RCLike.charZero_rclike instCharZero SemilinearMapClass.distribMulActionSemiHomClass RingHomClass.toLinearMapClassNNRat RingHom.instRingHomClass AlgHom.subsingleton Unique.instSubsingleton
slitPlane_eq_union 📖	mathematical	—	slitPlane Set Complex Set.instUnion setOf Real Real.instLT Real.instZero re im	—	Set.setOf_or
slitPlane_ne_zero 📖	—	Complex Set Set.instMembership slitPlane	—	—	zero_notMem_slitPlane
subset_slitPlane_iff_of_subset_sphere 📖	mathematical	Set Complex Set.instHasSubset Metric.sphere SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField instZero	slitPlane Set.instMembership instNeg ofReal	—	Mathlib.Tactic.Contrapose.contrapose_iff₃ Mathlib.Tactic.Push.not_forall_eq sub_zero eq_coe_norm_of_nonneg neg_nonneg IsOrderedAddMonoid.toAddLeftMono RCLike.toIsOrderedAddMonoid norm_neg neg_neg norm_real Real.instIsOrderedAddMonoid
summable_conj 📖	mathematical	—	Summable Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing SummationFilter.unconditional	—	RCLike.summable_conj
summable_ofReal 📖	mathematical	—	Summable Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup ofReal Real Real.instAddCommMonoid Real.pseudoMetricSpace	—	RCLike.summable_ofReal
tendsto_normSq_cocompact_atTop 📖	mathematical	—	Filter.Tendsto Complex Real DFunLike.coe MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instSemiring Real.semiring MonoidWithZeroHom.funLike normSq Filter.cocompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Filter.atTop Real.instPreorder	—	norm_mul_self_eq_normSq Filter.Tendsto.atTop_mul_atTop₀ Real.instIsOrderedRing tendsto_norm_cocompact_atTop instProperSpace
uniformContinuous_im 📖	mathematical	—	UniformContinuous Complex Real PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Real.pseudoMetricSpace im	—	ContinuousLinearMap.uniformContinuous SeminormedAddCommGroup.to_isUniformAddGroup instIsUniformAddGroupReal
uniformContinuous_re 📖	mathematical	—	UniformContinuous Complex Real PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Real.pseudoMetricSpace re	—	ContinuousLinearMap.uniformContinuous SeminormedAddCommGroup.to_isUniformAddGroup instIsUniformAddGroupReal
uniformlyContinuous_im 📖	mathematical	—	UniformContinuous Complex Real PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Real.pseudoMetricSpace im	—	uniformContinuous_im
uniformlyContinuous_re 📖	mathematical	—	UniformContinuous Complex Real PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Real.pseudoMetricSpace re	—	uniformContinuous_re
zero_notMem_slitPlane 📖	mathematical	—	Complex Set Set.instMembership slitPlane instZero	—	ofReal_mem_slitPlane lt_irrefl

Filter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_ofReal_iff 📖	mathematical	—	Tendsto Complex Complex.ofReal nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Real Real.pseudoMetricSpace	—	Topology.IsClosedEmbedding.tendsto_nhds_iff IsUniformEmbedding.isClosedEmbedding Real.instCompleteSpace T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space Complex.instT2Space CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity Complex.isUniformEmbedding_ofReal
tendsto_ofReal_iff' 📖	mathematical	—	Tendsto RCLike.ofReal nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real Real.pseudoMetricSpace	—	Topology.IsClosedEmbedding.tendsto_nhds_iff IsUniformEmbedding.isClosedEmbedding Real.instCompleteSpace T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity RCLike.isUniformEmbedding_ofReal

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofReal 📖	mathematical	Filter.Tendsto Real nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	Complex Complex.ofReal SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField	—	Filter.tendsto_ofReal_iff

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
reProdIm 📖	mathematical	IsCompact Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.reProdIm	—	RingHomInvPair.ids Homeomorph.isCompact_preimage prod

NormedAlgebra

Definitions

Name	Category	Theorems
complexToReal 📖	CompOp	34 math math: unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le, Unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le, CStarAlgebra.mem_Icc_algebraMap_iff_norm_le, PositiveLinearMap.apply_le_of_isSelfAdjoint, CFC.tendsto_cfc_rpow_sub_one_log, selfAdjoint.expUnitaryPathToOne_apply, CStarAlgebra.norm_or_neg_norm_mem_spectrum, CStarAlgebra.nnnorm_le_iff_of_nonneg, IsSelfAdjoint.neg_algebraMap_norm_le_self, CStarAlgebra.norm_smul_two_inv_smul_add_four_unitary, CFC.log_monotoneOn, CFC.monotone_rpow, IsSelfAdjoint.sq_spectrumRestricts, CStarAlgebra.mem_Icc_algebraMap_iff_nnnorm_le, CFC.rpow_le_rpow, selfAdjoint.star_coe_unitarySelfAddISMul, CStarAlgebra.rpow_neg_one_le_rpow_neg_one, CStarAlgebra.mul_star_le_algebraMap_norm_sq, IsSelfAdjoint.instIsometricContinuousFunctionalCalculus, CStarAlgebra.norm_le_iff_le_algebraMap, CStarAlgebra.star_mul_le_algebraMap_norm_sq, CStarAlgebra.rpow_neg_one_le_one, IsSelfAdjoint.map_spectrum_real, CFC.log_le_log, IsSelfAdjoint.toReal_spectralRadius_eq_norm, IsSelfAdjoint.self_add_I_smul_cfcSqrt_sub_sq_mem_unitary, CStarAlgebra.norm_mem_spectrum_of_nonneg, IsSelfAdjoint.le_algebraMap_norm_self, CFC.conjugate_rpow_neg_one_half, le_iff_norm_sqrt_mul_rpow, Unitary.path_apply, CStarAlgebra.nnnorm_mem_spectrum_of_nonneg, SpectrumRestricts.nnreal_iff_nnnorm, le_iff_norm_sqrt_mul_sqrt_inv

NormedSpace

Definitions

Name	Category	Theorems
complexToReal 📖	CompOp	256 math math: TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq, isConformalMap_conj, Complex.restrictScalars_one_smulRight', IsSelfAdjoint.quasispectrumRestricts, mellin_eq_fourier, SchwartzMap.integral_sesq_fourier_fourier, Real.hasFDerivAt_fourierChar_neg_bilinear_left, Complex.linearEquiv_det_conjLIE, CFC.monotoneOn_one_sub_one_add_inv, Real.fderiv_fourierIntegral, Complex.ofRealCLM_coe, SchwartzMap.inner_fourier_toL2_eq, SchwartzMap.toLp_fourierTransformInv_eq, Real.fourierIntegralInv_eq', CFC.monotone_nnrpow, Complex.integral_boundary_rect_eq_zero_of_differentiableOn, Complex.ofRealLI_apply, Real.fourierIntegral_eq, HasDerivWithinAt.complexToReal_fderiv', circleIntegral_def_Icc, Unitization.real_cfcₙ_eq_cfc_inr, SchwartzMap.lineDerivOp_fourier_eq, SchwartzMap.integral_bilin_fourierInv_eq, Complex.ofRealCLM_norm, HasDerivAt.comp_ofReal, rotation_injective, Complex.convexHull_reProdIm, Complex.conjLIE_apply, Complex.hasStrictFDerivAt_exp_real, MeasureTheory.ComplexMeasure.HaveLebesgueDecomposition.imPart, Real.vector_fourierIntegral_eq_integral_exp_smul, Real.fourier_real_eq_integral_exp_smul, isSelfAdjoint_iff_isStarNormal_and_spectrumRestricts, tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support, rotation_apply, toMatrix_rotation, SchwartzMap.integral_fourierInv_smul_eq, SchwartzMap.inner_toL2_toL2_eq, Complex.integral_circleTransform, SchwartzMap.integral_bilin_fourierIntegral_eq, SchwartzMap.toLp_fourierInv_eq, VectorFourier.fourierPowSMulRight_eq_comp, Complex.reCLM_nnnorm, Complex.deriv_ofReal_cpow_const, SchwartzMap.integral_sesq_fourier_eq, Real.fderiv_fourier, DiffContOnCl.circleAverage, SchwartzMap.fourier_lineDerivOp_eq, TemperedDistribution.instLineDerivLeftSMulReal, SchwartzMap.integral_norm_sq_fourier, mellin_hasDerivAt_of_isBigO_rpow, Complex.reCLM_coe, VectorFourier.hasFDerivAt_fourierIntegral, Real.circleAverage_eq_circleIntegral, Complex.equivRealProdCLM_symm_apply, tendsto_integral_exp_smul_cocompact, SchwartzMap.norm_fourier_toL2_eq, SchwartzMap.instFourierPair, Real.fourier_real_eq, Real.tendsto_integral_gaussian_smul', Real.hasFDerivAt_fourier, VectorFourier.differentiable_fourierIntegral, SchwartzMap.norm_fourierTransformCLM_toL2_eq, Real.fourier_mul_convolution_eq, VectorFourier.iteratedFDeriv_fourierIntegral, MeasureTheory.ComplexMeasure.equivSignedMeasure_apply, Real.differentiable_fourierIntegral, selfAdjoint.unitarySelfAddISMul_coe, HasDerivWithinAt.complexToReal_fderiv, TemperedDistribution.fourier_toTemperedDistributionCLM_eq, Complex.ofRealCLM_nnnorm, Complex.imCLM_norm, SchwartzMap.convolution_apply, TemperedDistribution.fourierTransformInv_toTemperedDistributionCLM_eq, SchwartzMap.integral_bilin_fourier_eq, SchwartzMap.fourierInv_apply_eq, HasDerivAt.complexToReal_fderiv', SchwartzMap.toTemperedDistributionCLM_apply_apply, HasDerivAt.complexToReal_fderiv, Real.fourierIntegral_real_eq_integral_exp_smul, MeasureTheory.SignedMeasure.re_toComplexMeasure, CStarAlgebra.instNonnegSpectrumClass, fourierIntegral_eq_half_sub_half_period_translate, Real.contDiff_fourierIntegral, Complex.ofRealCLM_apply, differentiableAt_complex_iff_differentiableAt_real, cfcHom_real_eq_restrict, IsSelfAdjoint.spectrumRestricts, VectorFourier.integral_sesq_fourierIntegral_eq_neg_flip, Complex.restrictScalars_one_smulRight, VectorFourier.fderiv_fourierIntegral, SchwartzMap.fourierInv_lineDerivOp_eq, VectorFourier.integral_fourierIntegral_swap, linear_isometry_complex, rotationOf_rotation, CFC.monotoneOn_one_sub_one_add_inv_real, SpectrumRestricts.real_iff, DiffContOnCl.circleAverage_smul_div, Real.fourier_eq, SchwartzMap.fourier_evalCLM_eq, QuasispectrumRestricts.real_iff, TemperedDistribution.instLineDerivSMulReal, tendsto_integral_exp_smul_cocompact_of_inner_product, SchwartzMap.instContinuousFourierInv, ContDiffAt.harmonicAt, VectorFourier.fourierSMulRight_apply, TemperedDistribution.lineDerivOp_toTemperedDistributionCLM_eq, isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts, MeasureTheory.ComplexMeasure.HaveLebesgueDecomposition.rePart, RCLike.complexLinearIsometryEquiv_symm_apply, Real.fourier_bilin_convolution_eq, mellin_eq_fourierIntegral, MeasureTheory.AEStronglyMeasurable.fourierPowSMulRight, SchwartzMap.integral_sesq_fourierIntegral_eq, Real.fourierIntegral_eq', VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral', Real.contDiff_fourier, Complex.conjCLE_nnorm, HasStrictDerivAt.complexToReal_fderiv', selfAdjoint.star_coe_unitarySelfAddISMul, rotation_trans, Complex.restrictScalars_toSpanSingleton, VectorFourier.contDiff_fourierIntegral, HasDerivAt.ofReal_comp, DifferentiableAt.ofReal_cpow_const, MeasureTheory.AEStronglyMeasurable.fourierSMulRight, rotationOf_coe, Unitization.nnreal_cfcₙ_eq_cfc_inr, isConformalMap_complex_linear_conj, mellin_comp_rpow, cfcₙHom_real_eq_restrict, MeasureTheory.ComplexMeasure.im_apply, fourierCoeff_eq_intervalIntegral, CStarAlgebra.conjugate_le_norm_smul', Complex.conjCLE_enorm, SchwartzMap.inner_fourierTransformCLM_toL2_eq, CFC.nnrpow_le_nnrpow, Real.tendsto_integral_cexp_sq_smul, Real.iteratedFDeriv_fourier, circleAverage_sub_sub_inv_smul_of_differentiable_on, SchwartzMap.convolution_continuous_left, SchwartzMap.integral_fourier_mul_eq, Complex.wedgeIntegral_add_wedgeIntegral_eq, Complex.integral_boundary_rect_eq_zero_of_differentiable_on_off_countable, Real.hasFDerivAt_fourierIntegral, linearEquiv_det_rotation, Complex.conjCLE_apply, SchwartzMap.fourier_coe, CStarAlgebra.star_left_conjugate_le_norm_smul, SchwartzMap.lineDerivOp_fourierInv_eq, Real.fourier_bilin_convolution_eq_integral, SchwartzMap.fourierInv_coe, Real.tendsto_integral_exp_smul_cocompact, Complex.imCLM_coe, SchwartzMap.toLp_fourierTransform_eq, fourierIntegral_half_period_translate, isBigO_deriv_ofReal_cpow_const_atTop, hasDerivAt_ofReal_cpow_const, SchwartzMap.instFourierSMul, SchwartzMap.fourierTransformCLM_apply, TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq, SchwartzMap.fderivCLM_fourier_eq, CStarModule.inner_mul_inner_swap_le, circleAverage_of_differentiable_on_off_countable, VectorFourier.integral_bilin_fourierIntegral_eq_flip, CFC.monotone_sqrt, CStarAlgebra.instNonnegSpectrumClass', CStarAlgebra.conjugate_le_norm_smul, Complex.equivRealProdCLM_symm_apply_re, norm_cfcₙ_one_sub_one_add_inv_lt_one, SchwartzMap.integral_fourierInv_mul_eq, TemperedDistribution.laplacian_toTemperedDistributionCLM_eq, VectorFourier.fourierPowSMulRight_apply, SchwartzMap.convolution_flip, SchwartzMap.integral_fourier_smul_eq, Complex.imCLM_nnnorm, VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral, SchwartzMap.instFourierInvAdd, TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq, Real.iteratedFDeriv_fourierIntegral, hasDerivAt_ofReal_cpow_const', CFC.sqrt_le_sqrt, MeasureTheory.ComplexMeasure.absolutelyContinuous_ennreal_iff, Complex.conjCLE_norm, MeasureTheory.Lp.toTemperedDistribution_toLp_eq, Real.tendsto_integral_gaussian_smul, Complex.imCLM_enorm, tendsto_integral_exp_inner_smul_cocompact, det_rotation, Continuous.fourierPowSMulRight, integral_complex_ofReal, VectorFourier.fourierIntegral_probChar, SchwartzMap.instFourierInvPair, VectorFourier.norm_fourierSMulRight_le, IsSelfAdjoint.self_add_I_smul_cfcSqrt_sub_sq_mem_unitary, RCLike.toContinuousLinearMap_complexLinearIsometryEquiv, Complex.ofRealCLM_enorm, Fourier.fourierIntegral_def, MeasureTheory.ComplexMeasure.re_apply, fourierCoeffOn_eq_integral, conformalAt_iff_differentiableAt_or_differentiableAt_comp_conj, AnalyticAt.harmonicAt, rotation_symm, VectorFourier.norm_fourierPowSMulRight_le, Complex.equivRealProdCLM_symm_apply_im, Real.hasFDerivAt_fourierChar_neg_bilinear_right, SchwartzMap.integral_inner_fourier_fourier, VectorFourier.norm_fourierSMulRight, MeasureTheory.Lp.toTemperedDistribution_apply, SchwartzMap.fourier_fderivCLM_eq, SchwartzMap.fourier_convolution_apply, Complex.hasStrictFDerivAt_log_real, SchwartzMap.instContinuousFourier, circleAverage_of_differentiable_on, CStarAlgebra.star_right_conjugate_le_norm_smul, Complex.reCLM_norm, MeasureTheory.ComplexMeasure.toComplexMeasure_to_signedMeasure, VectorFourier.integral_fourierIntegral_smul_eq_flip, SchwartzMap.coe_apply, Complex.integral_boundary_rect_eq_zero_of_continuousOn_of_differentiableOn, isTheta_deriv_ofReal_cpow_const_atTop, DifferentiableAt.conformalAt, Complex.imCLM_apply, Real.fourierInv_eq, isConformalMap_complex_linear, SchwartzMap.tsum_eq_tsum_fourierIntegral, CFC.monotoneOn_cfcₙ_rpowIntegrand₀₁, SchwartzMap.instFourierInvSMul, HasStrictDerivAt.complexToReal_fderiv, Real.fourierInv_eq', Complex.reCLM_enorm, VectorFourier.hasFDerivAt_fourierChar_smul, Real.fourierIntegral_real_eq, IsSelfAdjoint.instNonUnitalIsometricContinuousFunctionalCalculus, circleAverage_sub_sub_inv_smul_of_differentiable_on_off_countable, SchwartzMap.fourier_convolution, VectorFourier.integrable_fourierPowSMulRight, Real.fourierIntegralInv_eq, SchwartzMap.toLp_fourier_eq, isConformalMap_iff_is_complex_or_conj_linear, Real.fourier_eq', Real.differentiable_fourier, le_iff_norm_sqrt_mul_rpow, Real.fourier_smul_convolution_eq, Complex.det_conjLIE, SchwartzMap.instFourierAdd, Complex.equivRealProdCLM_apply, Complex.conjCLE_coe, MeasureTheory.SignedMeasure.im_toComplexMeasure, RCLike.complexLinearIsometryEquiv_apply, SchwartzMap.tsum_eq_tsum_fourier, le_iff_norm_sqrt_mul_sqrt_inv, Complex.restrictScalars_toSpanSingleton', Complex.rectangle_eq_convexHull, Complex.reCLM_apply, Complex.conjLIE_symm

RCLike

Definitions

Name	Category	Theorems
complexLinearIsometryEquiv 📖	CompOp	3 math math: complexLinearIsometryEquiv_symm_apply, toContinuousLinearMap_complexLinearIsometryEquiv, complexLinearIsometryEquiv_apply
complexRingEquiv 📖	CompOp	5 math math: sqrt_eq_ite, complexRingEquiv_apply, complexLinearIsometryEquiv_symm_apply, complexRingEquiv_symm_apply, complexLinearIsometryEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
I_to_complex 📖	mathematical	—	I Complex Complex.instRCLike Complex.I	—	—
complexLinearIsometryEquiv_apply 📖	mathematical	DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike im I Real.instOne	LinearIsometryEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedSpace.toModule Real.normedField NormedAlgebra.toNormedSpace SeminormedCommRing.toSeminormedRing toNormedAlgebra NormedSpace.complexToReal NormedField.toNormedSpace EquivLike.toFunLike LinearIsometryEquiv.instEquivLike complexLinearIsometryEquiv Equiv.toFun RingEquiv.toEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Complex.instMul Distrib.toAdd Complex.instAdd complexRingEquiv	—	RingHomInvPair.ids
complexLinearIsometryEquiv_symm_apply 📖	mathematical	DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike im I Real.instOne	LinearIsometryEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedSpace.toModule Real.normedField NormedSpace.complexToReal NormedField.toNormedSpace NormedAlgebra.toNormedSpace SeminormedCommRing.toSeminormedRing toNormedAlgebra EquivLike.toFunLike LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm complexLinearIsometryEquiv Equiv.invFun RingEquiv.toEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Complex.instMul Distrib.toAdd Complex.instAdd complexRingEquiv	—	RingHomInvPair.ids
complexRingEquiv_apply 📖	mathematical	DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike im I Real.instOne	RingEquiv Complex Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing Complex.instMul Distrib.toAdd Complex.instAdd EquivLike.toFunLike RingEquiv.instEquivLike complexRingEquiv Complex.ofReal re Complex.I	—	—
complexRingEquiv_symm_apply 📖	mathematical	DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike im I Real.instOne	RingEquiv Complex Complex.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing Complex.instAdd Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm complexRingEquiv ofReal Complex.re Complex.im	—	—
conj_tsum 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField RingHom.instFunLike starRingEnd toStarRing tsum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing	—	tsum_star instContinuousStar TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
hasSum_conj 📖	mathematical	—	HasSum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField RingHom.instFunLike starRingEnd toStarRing	—	ContinuousLinearEquiv.hasSum RingHomInvPair.ids
hasSum_conj' 📖	mathematical	—	HasSum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField RingHom.instFunLike starRingEnd toStarRing	—	ContinuousLinearEquiv.hasSum' RingHomInvPair.ids
hasSum_iff 📖	mathematical	—	HasSum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Real Real.instAddCommMonoid Real.pseudoMetricSpace DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike re im	—	hasSum_re hasSum_im re_add_im HasSum.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing hasSum_ofReal HasSum.mul_right
hasSum_im 📖	mathematical	HasSum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing	Real Real.instAddCommMonoid Real.pseudoMetricSpace DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike im	—	ContinuousLinearMap.hasSum
hasSum_ofReal 📖	mathematical	—	HasSum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing ofReal Real Real.instAddCommMonoid Real.pseudoMetricSpace	—	ofReal_re ContinuousLinearMap.hasSum
hasSum_re 📖	mathematical	HasSum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing	Real Real.instAddCommMonoid Real.pseudoMetricSpace DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike re	—	ContinuousLinearMap.hasSum
im_eq_complex_im 📖	mathematical	—	DFunLike.coe AddMonoidHom Complex Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField Complex.instRCLike AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike im Complex.im	—	—
im_to_complex 📖	mathematical	—	DFunLike.coe AddMonoidHom Complex Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField Complex.instRCLike AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike im Complex.im	—	—
im_tsum 📖	mathematical	Summable ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing	DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike im tsum Real.instAddCommMonoid Real.pseudoMetricSpace	—	ContinuousLinearMap.map_tsum TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
isUniformEmbedding_ofReal 📖	mathematical	—	IsUniformEmbedding Real PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField ofReal	—	Isometry.isUniformEmbedding LinearIsometry.isometry
map_nonneg_iff 📖	mathematical	DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike im I Real.instOne	Preorder.toLE PartialOrder.toPreorder toPartialOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace toNormedAlgebra ContinuousLinearMap.funLike map	—	nonneg_iff map_add AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass ofReal_re mul_re I_re MulZeroClass.mul_zero ofReal_im mul_one sub_self add_zero mul_im zero_add
normSq_to_complex 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom Complex Real NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField Complex.instRCLike Real.semiring MonoidWithZeroHom.funLike normSq Complex.instSemiring Complex.normSq	—	—
norm_to_complex 📖	mathematical	—	Norm.norm Complex Complex.instNorm Complex.instAdd Complex.ofReal DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike re Complex.instMul im Complex.I NormedField.toNorm	—	I_eq_zero_or_im_I_eq_one re_add_im im_eq_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MulZeroClass.zero_mul add_zero ofReal_re ofReal_im Complex.norm_real norm_algebraMap' NormedDivisionRing.to_normOneClass LinearIsometryEquiv.norm_map RingHomInvPair.ids
ofReal_eq_complex_ofReal 📖	mathematical	—	ofReal Complex Complex.instRCLike Complex.ofReal	—	—
ofReal_tsum 📖	mathematical	—	ofReal tsum Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing	—	Function.LeftInverse.map_tsum TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace DistribMulActionSemiHomClass.toAddMonoidHomClass charZero_rclike SemilinearMapClass.distribMulActionSemiHomClass RingHomClass.toLinearMapClassNNRat RingHom.instRingHomClass ContinuousLinearMap.continuous continuous_re ofReal_re
re_eq_complex_re 📖	mathematical	—	DFunLike.coe AddMonoidHom Complex Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField Complex.instRCLike AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike re Complex.re	—	—
re_to_complex 📖	mathematical	—	DFunLike.coe AddMonoidHom Complex Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField Complex.instRCLike AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike re Complex.re	—	—
re_tsum 📖	mathematical	Summable ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing	DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike re tsum Real.instAddCommMonoid Real.pseudoMetricSpace	—	ContinuousLinearMap.map_tsum TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
summable_conj 📖	mathematical	—	Summable ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField RingHom.instFunLike starRingEnd toStarRing	—	summable_star_iff instContinuousStar
summable_ofReal 📖	mathematical	—	Summable ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing ofReal Real Real.instAddCommMonoid Real.pseudoMetricSpace	—	ofReal_re ContinuousLinearMap.summable
toContinuousLinearMap_complexLinearIsometryEquiv 📖	mathematical	DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike im I Real.instOne	ContinuousLinearEquiv.toContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Complex Complex.instNormedField NormedSpace.toModule Real.normedField NormedAlgebra.toNormedSpace SeminormedCommRing.toSeminormedRing toNormedAlgebra NormedSpace.complexToReal NormedField.toNormedSpace LinearIsometryEquiv.toContinuousLinearEquiv complexLinearIsometryEquiv map Complex.instRCLike	—	RingHomInvPair.ids
to_complex_nonneg_iff 📖	mathematical	—	Complex Preorder.toLE PartialOrder.toPreorder Complex.partialOrder Complex.instZero Complex.instAdd Complex.ofReal DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike re Complex.instMul im Complex.I toPartialOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing	—	map_nonneg_iff

imaginaryPart

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_le 📖	mathematical	—	Real Real.instLE Norm.norm AddSubgroup AddCommGroup.toAddGroup SeminormedAddCommGroup.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint SeminormedAddCommGroup.toNorm AddSubgroup.seminormedAddCommGroup DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal NormedSpace.toModule Complex Complex.instNormedField selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing StarRing.toStarAddMonoid instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike imaginaryPart	—	instTrivialStarReal StarModule.complexToReal smul_neg map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass realPart_I_smul neg_neg norm_neg norm_smul NormedSpace.toNormSMulClass Complex.norm_I one_mul realPart.norm_le

realPart

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_le 📖	mathematical	—	Real Real.instLE Norm.norm AddSubgroup AddCommGroup.toAddGroup SeminormedAddCommGroup.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint SeminormedAddCommGroup.toNorm AddSubgroup.seminormedAddCommGroup DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal NormedSpace.toModule Complex Complex.instNormedField selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing StarRing.toStarAddMonoid instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike realPart	—	instTrivialStarReal StarModule.complexToReal Nat.instAtLeastTwoHAddOfNat inv_mul_cancel_left₀ two_ne_zero CharZero.NeZero.two RCLike.charZero_rclike AddSubgroup.norm_coe realPart_apply_coe norm_smul NormedSpace.toNormSMulClass norm_inv Real.norm_ofNat mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing LE.le.trans norm_add_le norm_star two_mul le_of_lt inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo

---

← Back to Index