Norm

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

Statistics

Metric	Count
Definitions cauSeqConj, cauSeqIm, cauSeqNorm, cauSeqRe, instNorm, instNormedAddCommGroup, limAux	7
Theorems abs_im_div_norm_le_one, abs_im_eq_norm, abs_im_le_norm, abs_im_lt_norm, abs_re_div_norm_le_one, abs_re_eq_norm, abs_re_le_norm, abs_re_lt_norm, dist_conj_self, dist_eq, dist_eq_re_im, dist_mk, dist_of_im_eq, dist_of_re_eq, dist_self_conj, edist_of_im_eq, edist_of_re_eq, equiv_limAux, im_le_norm, instIsComplete, isAbsoluteValueNorm, isCauSeq_conj, isCauSeq_im, isCauSeq_norm, isCauSeq_re, lim_conj, lim_eq_lim_im_add_lim_re, lim_im, lim_norm, lim_re, ne_zero_of_one_lt_re, ne_zero_of_re_pos, nndist_conj_self, nndist_of_im_eq, nndist_of_re_eq, nndist_self_conj, nnnorm_I, nnnorm_natCast, nnnorm_nnratCast, nnnorm_ofNat, nnnorm_ratCast, nnnorm_real, normSq_eq_norm_sq, normSq_ofReal_add_I_mul_sqrt_one_sub, normSq_ofReal_sub_I_mul_sqrt_one_sub, norm_I, norm_add_le', norm_add_mul_I, norm_conj, norm_def, norm_div, norm_eq_sqrt_sq_add_sq, norm_eq_zero_iff, norm_intCast, norm_int_of_nonneg, norm_le_abs_re_add_abs_im, norm_le_sqrt_two_mul_max, norm_map_zero', norm_mul, norm_mul_self_eq_normSq, norm_natCast, norm_neg', norm_nnratCast, norm_nonneg, norm_ofNat, norm_of_nonneg, norm_pow, norm_prod, norm_ratCast, norm_real, norm_sub_one_sq_eqOn_sphere, norm_sub_one_sq_eq_of_norm_eq_one, norm_sub_one_sq_eq_of_norm_one, norm_two, norm_zpow, one_le_normSq_iff, one_lt_normSq_iff, range_norm, range_normSq, re_le_norm, re_neg_ne_zero_of_one_lt_re, re_neg_ne_zero_of_re_pos, sq_norm, sq_norm_sub_sq_im, sq_norm_sub_sq_re	85
Total	92

Complex

Definitions

Name	Category	Theorems
cauSeqConj 📖	CompOp	1 math math: lim_conj
cauSeqIm 📖	CompOp	2 math math: lim_im, lim_eq_lim_im_add_lim_re
cauSeqNorm 📖	CompOp	1 math math: lim_norm
cauSeqRe 📖	CompOp	2 math math: lim_re, lim_eq_lim_im_add_lim_re
instNorm 📖	CompOp	398 math math: norm_conj, HadamardThreeLines.norm_le_interpStrip_of_mem_verticalClosedStrip_eps, CuspFormClass.qExpansion_isBigO, norm_log_one_sub_inv_add_logTaylor_neg_le, Polynomial.mahlerMeasure_const, Polynomial.mahlerMeasure_def_of_ne_zero, tendsto_log_nhdsWithin_im_neg_of_re_neg_of_im_zero, norm_circleTransformBoundingFunction_le, log_re, EisensteinSeries.linear_inv_isBigO_left, DiffContOnCl.circleAverage_poissonKernel_smul', ModularFormClass.qExpansionFormalMultilinearSeries_apply_norm, lim_conj, GaussianFourier.norm_cexp_neg_mul_sq_add_mul_I, MeasureTheory.taylor_charFun_two, Int.cast_complex_isTheta_cast_real, norm_sub_one_sq_eq_of_norm_eq_one, norm_polarCoord_symm, norm_sub_eq, instIsComplete, summable_riemannZetaSummand, Polynomial.norm_leadingCoeff_eq_one_of_mahlerMeasure_eq_one, norm_le_abs_re_add_abs_im, norm_jacobiTheta₂_term_le, norm_sub_mem_Icc_angle, isTheta_cpow_rpow, Polynomial.mahlerMeasure_eq_leadingCoeff_mul_prod_roots, isLittleO_exp_neg_mul_sq_cocompact, norm_jacobiTheta₂_term_fderiv_ge, norm_mul_self_eq_normSq, norm_nonneg, NumberField.InfinitePlace.le_iff_le, NumberField.norm_norm_le_norm_mul_house_pow, countingFunction_finsum_eq_finsum_add, ModularGroup.coe_fd, OnePoint.isBoundedAt_iff_exists_SL2Z, locally_lipschitz_exp, one_le_normSq_iff, Polynomial.logMahlerMeasure_C_mul, norm_eq_zero_iff, EisensteinSeries.summand_bound_of_mem_verticalStrip, Function.Periodic.norm_qParam_le_of_one_half_le_im, arg_of_re_nonneg, UpperHalfPlane.isOpenMap_norm, Polynomial.one_le_prod_max_one_norm_roots, circleAverage_log_norm_sub_const₁, norm_eq_one_iff', AnalyticOnNhd.circleAverage_log_norm, norm_cexp_neg_mul_sq, Real.norm_exp_I_mul_ofReal_sub_one_le, norm_one_add_mul_inv_le, circleAverage_log_norm_sub_const_of_mem_closedBall, norm_cos_add_sin_mul_I, Function.Periodic.norm_qParam_lt_iff, norm_pow, DirichletCharacter.norm_LSeries_product_ge_one, isCauSeq_conj, integrableOn_Ioi_norm_cpow_of_lt, OnePoint.isBoundedAt_iff_forall_SL2Z, integral_rpow_mul_exp_neg_rpow, exp_def, volume_sum_rpow_le, norm_log_one_add_le, mul_angle_le_norm_sub, NumberField.mixedEmbedding.convexBodySumFun_apply', Polynomial.logMahlerMeasure_of_degree_eq_one, sin_bound, circleAverage_log_norm_sub_const_eq_log_radius_add_posLog, LindemannWeierstrass.exp_polynomial_approx, mul_conj', arg_of_re_neg_of_im_nonneg, NumberField.exists_conjugate_one_le_norm, NumberField.InfinitePlace.norm_embedding_eq, PeriodPair.weierstrassP_bound, deriv_norm_ofReal_cpow, re_herglotzRieszKernel_le, norm_map_zero', norm_circleMap_zero, arg_of_im_pos, ClosedSubmodule.inner_real_eq_re_inner, integrableOn_Ioi_norm_cpow_iff, norm_natCast, norm_exp_I_mul_ofReal_sub_one, CuspFormClass.petersson_bounded_left, sq_norm_sub_sq_re, abs_re_eq_norm, norm_add_eq, norm_cpow_of_ne_zero, im_le_norm, norm_ofReal_cpow_eventually_eq_atTop, integral_exp_neg_rpow, norm_mul_cos_arg, sq_norm, norm_log_sub_logTaylor_le, exists_norm_eq_mul_self, Polynomial.logMahlerMeasure_X_sub_C, EisensteinSeries.summable_norm_eisSummand, Function.Periodic.boundedAtFilter_cuspFunction, norm_cpow_of_imp, norm_eq_one_iff, UpperHalfPlane.norm_σ, IsExpCmpFilter.isLittleO_exp_cpow, norm_log_one_add_sub_self_le, norm_jacobiTheta₂_term, polarCoord_apply, ValueDistribution.characteristic_sub_characteristic_inv_of_ne_zero, abs_im_le_norm, cpow_ofReal_re, norm_nnratCast, norm_add_eq_iff, Polynomial.logMahlerMeasure_X_add_C, equivRealProd_apply_le', sq_norm_sub_sq_im, LSeriesSummable.le_const_mul_rpow, normSq_eq_norm_sq, ValueDistribution.characteristic_sub_characteristic_inv_at_zero, abs_im_eq_norm, norm_cpow_real, UpperHalfPlane.IsZeroAtImInfty.petersson_exp_decay_left, isTheta_ofReal, isBigO_re_sub_re, norm_exp_mul_sq_le, circleAverage_log_norm_sub_const₀, isBigO_cpow_rpow, norm_exp_sub_sum_le_norm_mul_exp, Polynomial.intervalIntegrable_mahlerMeasure, HadamardThreeLines.norm_invInterpStrip, continuousOn_norm_circleTransformBoundingFunction, Function.Periodic.im_invQParam, UpperHalfPlane.norm_exp_two_pi_I_lt_one, arg_of_re_neg_of_im_neg, circleIntegrable_log_norm_factorizedRational, isCauSeq_norm_exp, Polynomial.mahlerMeasure_C_mul_X_add_C, tendsto_norm_tan_atTop, Polynomial.prod_max_one_norm_roots_le_mahlerMeasure_of_one_le_leadingCoeff, SlashInvariantForm.exists_one_half_le_im_and_norm_le, norm_jacobiTheta_sub_one_le, HadamardThreeLines.norm_le_interpStrip_of_mem_verticalClosedStrip, isBigO_riemannZeta_sub_one_div, OnePoint.isBoundedAt_iff, UnitDisc.instCanLiftCoeLtRealNormOfNat, ModularFormClass.exp_decay_sub_atImInfty, ModularFormClass.exists_petersson_le, IsExpCmpFilter.tendsto_norm, UpperHalfPlane.IsZeroAtImInfty.exp_decay_atImInfty, log_sub_self_isBigO, ClosedSubmodule.mem_symplComp_iff, ValueDistribution.characteristic_sub_characteristic_inv_le, arg_eq_nhds_of_im_neg, AnalyticOnNhd.circleAverage_log_norm_of_ne_zero, Polynomial.logMahlerMeasure_eq_log_leadingCoeff_add_sum_log_roots, arg_of_im_nonneg_of_ne_zero, isBigO_at_im_infty_jacobiTheta_sub_one, Polynomial.mahlerMeasure_X_add_C, eq_coe_norm_of_nonneg, OnePoint.isBoundedAt_infty_iff, norm_real, CuspFormClass.petersson_bounded_right, ModularFormClass.bdd_at_infty, UpperHalfPlane.norm_qParam_lt_one, conj_mul', hasSum_sq_fourierCoeffOn, LSeries.norm_term_eq, ProbabilityTheory.norm_complexMGF_le_mgf, ModularFormClass.exists_bound, EisensteinSeries.auxbound1, Polynomial.logMahlerMeasure_def, integral_exp_neg_mul_rpow, EisensteinSeries.norm_le_tsum_norm, norm_ratCast, norm_of_nonneg, abs_im_lt_norm, EisensteinSeries.isBoundedAtImInfty_eisensteinSeries_SIF, summable_dirichletSummand, norm_mul_cos_add_sin_mul_I, norm_sub_le_angle, norm_zpow, volume_sum_rpow_lt, Polynomial.quadratic_dvd_of_aeval_eq_zero_im_ne_zero, ValueDistribution.characteristic_sub_characteristic_inv, EisensteinSeries.linear_inv_isBigO_right_add, UpperHalfPlane.petersson_norm_symm, MeasureTheory.norm_charFun_le_one, cos_bound, norm_mul_exp_arg_mul_I, dist_eq, cpow_inv_two_im_eq_sqrt, cpow_inv_two_re, Circle.norm_coe, arg_eq_arg_iff, EisensteinSeries.isBigO_linear_add_const_vec, norm_natCast_cpow_of_pos, EisensteinSeries.auxbound2, norm_div, HadamardThreeLines.norm_le_interpStrip_of_mem_verticalStrip_zero, isBigO_im_sub_im, cexp_neg_quadratic_isLittleO_abs_rpow_cocompact, angle_le_mul_norm_sub, EisensteinSeries.r_mul_max_le, norm_exp_ofReal, GaussianFourier.norm_cexp_neg_mul_sq_add_mul_I', norm_prime_cpow_le_one_half, norm_ofNat, norm_canonicalFactor_eval_circle_eq_one, isTheta_ofReal_right, Polynomial.sum_sq_norm_coeff_eq_circleAverage, Polynomial.mahlerMeasure_X_sub_C, exp_sub_sum_range_succ_isLittleO_pow, MeasureTheory.measureReal_abs_gt_le_integral_charFun, isBigO_ofReal_left, rotationOf_coe, norm_def, isBigO_comp_ofReal_nhds_ne, abs_im_div_norm_le_one, norm_int_of_nonneg, CuspFormClass.exists_bound, IsExpCmpFilter.isLittleO_log_norm_re, circleAverage_log_norm_add_const_eq_posLog, norm_natCast_cpow_pos_of_pos, re_le_norm, norm_add_mul_I, MeromorphicOn.circleAverage_log_norm, abs_re_le_norm, exp_sub_sum_range_isBigO_pow, tendsto_norm_tan_of_cos_eq_zero, DirichletCharacter.norm_LFunction_product_ge_one, IsExpCmpFilter.isLittleO_zpow_mul_exp, MeasureTheory.measureReal_abs_dual_gt_le_integral_charFunDual, Function.locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const, EisensteinSeries.linear_isTheta_left, norm_of_nonneg', exp_bound, MeasureTheory.norm_one_sub_charFun_le_two, exists_norm_mul_eq_self, isTheta_cpow_const_rpow, arg_of_im_neg, norm_sub_one_sq_eqOn_sphere, ValueDistribution.proximity_zero_of_complexValued, sqrt_eq_real_add_ite, ext_norm_arg_iff, norm_jacobiTheta₂'_term_le, NumberField.canonicalEmbedding.norm_le_iff, NumberField.mixedEmbedding.normAtPlace_apply_of_isComplex, re_eq_neg_norm, tsum_sq_fourierCoeffOn, EisensteinSeries.linear_isTheta_right_add, norm_exp_sub_one_le, integrable_pow_mul_norm_one_add_mul_inv, circleAverage_log_norm_sub_const_eq_posLog, norm_exp, lim_im, circleAverage_log_norm_factorizedRational, PhragmenLindelof.isBigO_sub_exp_rpow, isBigO_deriv_ofReal_cpow_const_atTop, Polynomial.leading_coeff_le_mahlerMeasure, AnalyticAt.harmonicAt_log_norm, AnalyticOnNhd.sum_divisor_le, MeasureTheory.measureReal_abs_inner_gt_le_integral_charFun, NumberField.norm_embedding_le_house, norm_sub_eq_iff, Polynomial.mahlerMeasure_of_degree_eq_one, LSeriesSummable.isBigO_rpow, norm_add_le', cexp_neg_quadratic_isLittleO_rpow_atTop, cpow_ofReal_im, exp_bound', circleAverage_log_norm_sub_const₂, norm_I, IsPrimitiveRoot.norm'_eq_one, ModularFormClass.qExpansion_isBigO, isCauSeq_im, norm_eq_one_of_mem_rootsOfUnity, range_norm, ModularGroup.exists_one_half_le_im_smul_and_norm_denom_le, HadamardThreeLines.eventuallyle, abs_re_lt_norm, one_lt_normSq_iff, Function.Periodic.norm_qParam, norm_exp_eq_iff_re_eq, ModularFormClass.bounded_at_infty_comp_ofComplex, CuspFormClass.exp_decay_atImInfty', arg_eq_nhds_of_im_pos, norm_cpow_inv_nat, integral_rpow_mul_exp_neg_mul_rpow, log_sub_logTaylor_isBigO, UnitDisc.norm_lt_one, ModularFormClass.bdd_at_infty_slash, UpperHalfPlane.IsZeroAtImInfty.exp_decay_atImInfty', hasSum_sq_fourierCoeff, RCLike.norm_to_complex, isBigO_ofReal_right, lim_norm, norm_log_one_sub_inv_sub_self_le, ValueDistribution.logCounting_zero_sub_logCounting_top_eq_circleAverage_sub_const, cpow_inv_two_im_eq_neg_sqrt, HadamardThreeLines.norm_le_interpStrip_of_mem_verticalClosedStrip₀₁, arg_eq_nhds_of_re_pos, SlashInvariantFormClass.norm_petersson_smul, Polynomial.logMahlerMeasure_const, DirichletCharacter.LFunctionTrivChar_isBigO_near_one_horizontal, norm_exp_sub_one_sub_id_le, norm_natCast_cpow_le_norm_natCast_cpow_iff, norm_natCast_cpow_le_norm_natCast_cpow_of_pos, norm_cpow_eq_rpow_re_of_nonneg, norm_exp_le_exp_norm, IsExpCmpFilter.isLittleO_cpow_exp, UnitAddTorus.hasSum_sq_mFourierCoeff, circleTransformDeriv_bound, norm_exp_mul_exp_add_exp_neg_le_of_abs_im_le, isCauSeq_norm, Polynomial.logMahlerMeasure_monomial, equiv_limAux, NumberField.InfinitePlace.eq_iff_eq, EisensteinSeries.linear_isTheta_right, norm_exp_sub_sum_le_exp_norm_sub_sum, Polynomial.logMahlerMeasure_C_mul_X_add_C, norm_log_natCast_le_rpow_div, arg_eq_nhds_of_re_neg_of_im_pos, norm_prod, volume_sum_rpow_lt_one, circleIntegrable_log_norm_sub_const, norm_exp_ofReal_mul_I, isTheta_ofReal_left, tendsto_log_nhdsWithin_im_nonneg_of_re_neg_of_im_zero, norm_log_one_add_half_le_self, isBigO_comp_ofReal_nhds, tsum_sq_fourierCoeff, IsExpCmpFilter.isLittleO_pow_mul_exp, norm_eq_sqrt_sq_add_sq, isTheta_deriv_ofReal_cpow_const_atTop, GaussianFourier.verticalIntegral_norm_le, borelCaratheodory, Polynomial.norm_root_le_one_of_mahlerMeasure_eq_one, CuspFormClass.exp_decay_atImInfty, LSeries.norm_term_le, norm_two, norm_cpow_le, arg_eq_nhds_of_re_neg_of_im_neg, isAbsoluteValueNorm, isLittleO_ofReal_right, DirichletCharacter.LFunction_isBigO_horizontal, Orientation.norm_kahler, Polynomial.norm_coeff_le_choose_mul_mahlerMeasure, ModularGroup.coe_fdo, abs_cpow_inv_two_im, norm_le_sqrt_two_mul_max, UpperHalfPlane.IsZeroAtImInfty.petersson_exp_decay_right, re_eq_norm, norm_exp_I_mul_ofReal, isCauSeq_exp, MeasureTheory.norm_charFun_le, norm_intCast, CStarAlgebra.exists_sum_four_unitary, norm_cpow_eq_rpow_re_of_pos, norm_mul, borelCaratheodory_zero, NumberField.mixedEmbedding.normAtComplexPlaces_apply_isComplex, norm_sub_one_sq_eq_of_norm_one, IsExpCmpFilter.isLittleO_cpow_mul_exp, ModularForm.summable_eta_q, norm_eq_one_of_pow_eq_one, UnitDisc.exists, qExpansion_coeff_isBigO_of_norm_isBigO, IsExpCmpFilter.isTheta_cpow_exp_re_mul_log, norm_neg', NumberField.InfinitePlace.apply, Polynomial.mahlerMeasure_le_sum_norm_coeff, EisensteinSeries.summand_bound, ModularFormClass.exp_decay_sub_atImInfty', neg_re_eq_norm, UpperHalfPlane.det_smulFDeriv, isCauSeq_re, integrableOn_Ioi_deriv_norm_ofReal_cpow, isLittleO_ofReal_left, sin_arg, NumberField.house.basis_repr_norm_le_const_mul_house, ValueDistribution.proximity_sub_proximity_inv_eq_circleAverage, cos_arg, UpperHalfPlane.IsBoundedAtImInfty.slash, norm_natCast_cpow_of_re_ne_zero, poissonKernel_def, Function.Periodic.exp_decay_sub_of_bounded_at_inf, abs_re_div_norm_le_one, UnitDisc.sq_norm_lt_one, Function.Periodic.exp_decay_of_zero_at_inf, cpow_ofReal, equivRealProd_apply_le, lim_re, le_re_herglotzRieszKernel, norm_jacobiTheta₂_term_fderiv_le, EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF, exp_bound_sq, EisensteinSeries.linear_inv_isBigO_right, norm_mul_sin_arg, lim_eq_lim_im_add_lim_re, LSeries.norm_term_le_of_re_le_re, ModularGroup.coe_truncatedFundamentalDomain
instNormedAddCommGroup 📖	CompOp	1055 math math: ArithmeticFunction.vonMangoldt.residueClass_eq, logDeriv_tprod_eq_tsum, HurwitzZeta.hasSum_int_hurwitzZetaOdd, NumberField.mixedEmbedding.integral_comp_polarSpaceCoord_symm, TemperedDistribution.lineDerivOpCLM_eq, NumberField.mixedEmbedding.fundamentalDomain_integerLattice, MeasureTheory.Lp.toTemperedDistributionCLM_apply, Orientation.kahler_map_complex, ContDiffAt.csin, UpperHalfPlane.mdifferentiable_num, TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq, hasSum_mellin_pi_mul_sq', cos_eq_tsum, ModularForm.mul_slash_SL2, EulerSine.integral_cos_mul_cos_pow, ModularForm.smul_slash, nnnorm_exp_I_mul_ofReal, NumberField.mixedEmbedding.normAtComplexPlaces_mixedSpaceOfRealSpace, restrictScalars_one_smulRight', meromorphicOrderAt_canonicalFactor, completedZeta_eq_tsum_of_one_lt_re, Distribution.dsupport_delta, IsSelfAdjoint.quasispectrumRestricts, CuspFormClass.holo, NumberField.mixedEmbedding.lintegral_comp_polarCoord_symm, MeasureTheory.charFun_eq_fourierIntegral', PeriodPair.hasFPowerSeriesAt_weierstrassPExcept, Real.hasFDerivAt_fourierChar_neg_bilinear_left, EisensteinSeries.hasSum_e2Summand_symmetricIcc, Real.fourierCoeff_tsum_comp_add, UnitAddTorus.coe_mFourierBasis, ModularFormClass.qExpansionFormalMultilinearSeries_apply_norm, ModularFormClass.hasFPowerSeries_cuspFunction, NumberField.canonicalEmbedding.mem_span_latticeBasis, iteratedDeriv_even_cosh, MeasureTheory.contDiff_charFun', ModularFormClass.qExpansionFormalMultilinearSeries_radius, PeriodPair.hasSumLocallyUniformly_weierstrassP, LSeries.term_sum, HurwitzZeta.hasSum_int_cosKernel₀, HurwitzZeta.hasSum_int_hurwitzZetaEven, ofRealCLM_coe, kahler, areaForm, finrank_real_complex_fact', Real.tsum_eq_tsum_fourier, PeriodPair.coeff_weierstrassPExceptSeries, complexOfReal_hasDerivWithinAt, analyticAt_cosh, SlashInvariantForm.slash_action_eq', ModularForm.mul_slash, meromorphic_digamma, has_pointwise_sum_fourier_series_of_summable, MeasureTheory.charFunDual_apply, norm_sub_mem_Icc_angle, PeriodPair.iteratedDeriv_weierstrassPExcept_self, LSeries.term_convolution', GammaIntegral_eq_mellin, PeriodPair.derivWeierstrassPExcept_sub, tsum_eisSummand_eq_riemannZeta_mul_eisensteinSeries, norm_jacobiTheta₂_term_fderiv_ge, NumberField.canonicalEmbedding.latticeBasis_apply, integral_comp_pi_polarCoord_symm, summableLocallyUniformlyOn_iteratedDerivWithin_cexp, PeriodPair.ω₁_div_two_notMem_lattice, ContDiffWithinAt.cexp, AnalyticOn.cpow, ValueDistribution.characteristic_mul_top_le, span_fourier_closure_eq_top, PeriodPair.basis_one, OnePoint.isBoundedAt_iff_exists_SL2Z, HasDerivWithinAt.complexToReal_fderiv', Orientation.kahler_comp_rightAngleRotation', one_add_cpow_hasFPowerSeriesAt_zero, tsum_exp_neg_mul_int_sq, UpperHalfPlane.analyticAt_smul, MeasureTheory.iteratedDeriv_charFun_zero, ContDiffOn.ccosh, analyticOn_sin, GaussianFourier.integral_cexp_neg_mul_sq_norm, Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay_of_summable, angle_exp_one, TemperedDistribution.fourierMultiplierCLM_smul, circleIntegral.integral_sub_inv_of_mem_ball, ValueDistribution.proximity_zero_mul_le, angle_div_right_eq_angle_mul_left, hasSum_one_div_nat_pow_mul_fourier, two_mul_riemannZeta_eq_tsum_int_inv_pow_of_even, nndist_self_conj, betaIntegral_scaled, GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace, fourierCoeffOn.const_mul, SlashInvariantForm.quotientFunc_mk, mellin_div_const, TemperedDistribution.lineDerivOp_fourier_eq, ModularForm.SL_slash, ofRealCLM_norm, ProbabilityTheory.hasDerivAt_integral_pow_mul_exp, NumberField.mixedEmbedding.mem_idealLattice, IsConformalMap.is_complex_or_conj_linear, AnalyticOnNhd.circleAverage_log_norm, iteratedDeriv_odd_sinh, convexHull_reProdIm, fourierIntegral_gaussian_innerProductSpace', fourier_gaussian_pi', MeasureTheory.charFun_eq_fourierIntegral, oangle, UnitAddTorus.mFourierSubalgebra_coe, TemperedDistribution.smulLeftCLM_compL_smulLeftCLM, iteratedDerivWithin_tsum_cexp_eq, PeriodPair.iteratedDeriv_derivWeierstrassPExcept_self, intervalIntegral.integral_ofReal, meromorphicOn_canonicalFactor, GaussianFourier.integral_cexp_neg_mul_sq_norm_add, PeriodPair.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept, PeriodPair.weierstrassP_coe, hasStrictFDerivAt_exp_real, ModularForm.prod_slash, MeasureTheory.ComplexMeasure.HaveLebesgueDecomposition.imPart, sum_cauchyPowerSeries_eq_integral, NumberField.mixedEmbedding.instIsAddHaarMeasureMixedSpaceVolume, UnitAddTorus.mFourierSubalgebra_closure_eq_top, nnnorm_ratCast, Distribution.IsVanishingOn.smulLeftCLM, tendsto_tsum_powerSeries_nhdsWithin_stolzCone, AnalyticWithinAt.cpow, angle_mul_left, analyticOnNhd_circleMap, NumberField.mixedEmbedding.commMap_apply_of_isComplex, hasSum_nat_jacobiTheta, TemperedDistribution.fourierMultiplierCLM_compL_fourierMultiplierCLM, differentiableOn_iteratedDerivWithin_cotTerm, PeriodPair.hasSum_derivWeierstrassPExcept, NumberField.mixedEmbedding.instNoAtomsMixedSpaceVolume, ValueDistribution.proximity_pow_zero, toBasis_orthonormalBasisOneI, ModularForm.prod_slash_sum_weights, HarmonicAt.analyticAt_complex_partial, NumberField.mixedEmbedding.convexBodyLT_volume, OnePoint.isBoundedAt_iff_forall_SL2Z, integral_rpow_mul_exp_neg_rpow, ZMod.completedLFunction_def_even, SchwartzMap.integral_fourierInv_smul_eq, SlashInvariantForm.quotientFunc_smul, volume_sum_rpow_le, PeriodPair.analyticAt_weierstrassPExcept, summableLocallyUniformlyOn_iteratedDerivWithin_cotTerm, SchwartzMap.inner_toL2_toL2_eq, analyticWithinAt_cosh, MeasureTheory.SignedMeasure.toComplexMeasure_apply, ModularForm.tsum_logDeriv_eta_q, EisensteinSeries.summable_left_one_div_linear_sub_one_div_linear, mul_angle_le_norm_sub, coe_orthonormalBasisOneI, Unitization.sqrt_inr, fourier_gaussian_innerProductSpace, OnePoint.isZeroAt_iff_exists_SL2Z, NumberField.mixedEmbedding.negAt_apply_snd, contDiff_cosh, analyticOn_cosh, EisensteinSeries.E2_slash_action, MeasureTheory.charFun_apply, CuspForm.coe_trace, EisensteinSeries.e2Summand_summable, TemperedDistribution.smulLeftCLM_neg, AnalyticAt.harmonicAt_im, cexp_tsum_eq_tprod, reCLM_nnnorm, nndist_of_im_eq, ContDiff.ccos, Function.HasTemperateGrowth.toTemperedDistribution_apply, NumberField.mixedEmbedding.negAt_preimage, hasDerivAt_GammaIntegral, LSeries_iteratedDeriv, starConvex_ofReal_slitPlane, CuspForm.coeHom_apply, analyticOnNhd_univ_iff_differentiable, NumberField.mixedEmbedding.fundamentalCone.volume_frontier_normLeOne, NumberField.mixedEmbedding.iUnion_negAt_plusPart_ae, HurwitzZeta.hasSum_nat_sinZeta, EisensteinSeries.G2_slash_action, MeasureTheory.charFun_apply_real, taylorSeries_eq_on_ball', fourierCoeff_bernoulli_eq, summable_conj, analyticOn_sinh, PeriodPair.latticeBasis_zero, ZMod.LFunction_def_odd, EulerSine.integral_cos_mul_cos_pow_aux, starConvex_one_slitPlane, TemperedDistribution.instLineDerivLeftSMulReal, LindemannWeierstrass.exp_polynomial_approx, MeasureTheory.iteratedFDeriv_charFun, NumberField.mixedEmbedding.stdBasis_apply_isComplex_snd, TemperedDistribution.fourierInv_lineDerivOp_eq, UpperHalfPlane.mdifferentiable_inv_denom, hasStrictFDerivAt_cpow', NumberField.mixedEmbedding.negAt_signSet_apply_isComplex, InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_complexPlane, NumberField.mixedEmbedding.fundamentalCone.volume_interior_eq_volume_closure, Orientation.kahler_eq_zero_iff, AddChar.sum_apply_eq_ite, PositiveLinearMap.preGNS_norm_def, ValueDistribution.proximity_inv, integral_comp_polarCoord_symm, PeriodPair.ω₂_div_two_notMem_lattice, UnitAddTorus.mFourierCoeff_toLp, PeriodPair.hasSum_derivWeierstrassP, PeriodPair.compl_lattice_diff_singleton_mem_nhds, NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq, NumberField.mixedEmbedding.convexBodySum_volume_eq_zero_of_le_zero, integral_exp_mul_complex_Ioi, setIntegral_Ioi_zero_cpow, TemperedDistribution.instFourierAdd, PeriodPair.hasSumLocallyUniformly_derivWeierstrassP, sameRay_of_arg_eq, SlashInvariantForm.coe_translate, NumberField.mixedEmbedding.normAtComplexPlaces_polarSpaceCoord_symm, TemperedDistribution.laplacian_eq_fourierMultiplierCLM, MeasureTheory.ComplexMeasure.singularPart_add_withDensity_rnDeriv_eq, ContDiff.cexp, Orientation.kahler_swap, PeriodPair.hasFPowerSeriesAt_derivWeierstrassPExcept, cauchyPowerSeries_apply, summable_eisSummand, LSeries_analyticOnNhd, TemperedDistribution.instFourierSMul, contDiff_circleMap, HurwitzZeta.hasSum_hurwitzZeta_of_one_lt_re, NumberField.mixedEmbedding.fundamentalCone.logMap_expMapBasis, AnalyticWithinAt.cexp, convex_halfSpace_re_le, reCLM_coe, AnalyticOnNhd.cpow, orthonormal_fourier, UpperHalfPlane.contMDiff_coe, CuspForm.holo', analyticAt_sin, Differentiable.hasFPowerSeriesOnBall, PeriodPair.mem_lattice, BoundedContinuousFunction.mem_charPoly, Orientation.kahler_comp_rightAngleRotation, EisensteinSeries.tsum_symmetricIco_linear_sub_linear_add_one_eq_zero, BoundedContinuousFunction.charAlgHom_apply, ArithmeticFunction.vonMangoldt.residueClass_apply, TemperedDistribution.delta_apply, PeriodPair.analyticOnNhd_derivWeierstrassPExcept, fourierIntegral_gaussian_pi, hasSum_mellin, iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow, integral_exp_mul_complex, DifferentiableOn.contDiffOn, real_linearMap_map_smul_complex, EisensteinSeries.G2_eq_tsum_symmetricIco, equivRealProdCLM_symm_apply, TemperedDistribution.instContinuousFourier, cos_eq_tsum', cot_series_rep', NumberField.canonicalEmbedding.integralBasis_repr_apply, integral_exp_neg_rpow, PeriodPair.basis_zero, NumberField.mixedEmbedding.negAt_signSet_apply_isReal, dist_self_conj, hasSum_jacobiTheta₂_term, hasFDerivAt_jacobiTheta₂_term, AnalyticAt.clog, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, UpperHalfPlane.contMDiff_inv_denom, gelfandStarTransform_symm_apply, orthonormalBasisOneI_repr_apply, HurwitzZeta.hasSum_nat_completedCosZeta, tendsto_sub_mul_tsum_nat_cpow, Summable_cotTerm, SchwartzMap.delta_apply, norm_cauchyPowerSeries_le, summable_jacobiTheta₂_term_fderiv_iff, fourier_gaussian_innerProductSpace', HurwitzZeta.hasSum_nat_hurwitzZetaEven, HurwitzZeta.hasSum_int_cosKernel, ZMod.completedLFunction_def_odd, hasSum_fourier_series_L2, NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis, PeriodPair.isClosed_lattice, integral_cpow, ProbabilityTheory.iteratedDeriv_complexMGF, NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIdealLattice, contDiffAt_log, convex_halfSpace_im_gt, GaussianFourier.integrable_cexp_neg_mul_sum_add, ContDiffOn.csin, hasStrictFDerivAt_cpow, differentiable_iteratedDeriv_sin, AddChar.expect_apply_eq_zero_iff_ne_zero, EisensteinSeries.linear_right_summable, ValueDistribution.characteristic_sub_characteristic_inv_of_ne_zero, PositiveLinearMap.preGNS_inner_def, LSeries_eq_mul_integral_of_nonneg, angle_mul_right, PeriodPair.periodic_derivWeierstrassP, EisensteinSeries.summable_linear_left_mul_linear_left, riemannZeta_eulerProduct_exp_log, HasStrictFDerivAt.cexp, iteratedDeriv_odd_sin, MeasureTheory.ComplexMeasure.equivSignedMeasure_apply, EulerSine.sin_pi_mul_eq, integral_mul_cexp_neg_mul_sq, NumberField.mixedEmbedding.span_idealLatticeBasis, NumberField.mixedEmbedding.fundamentalCone.norm_expMapBasis, ValueDistribution.characteristic_sub_characteristic_inv_at_zero, TemperedDistribution.fourierMultiplierCLM_fourierMultiplierCLM_apply, zeta_eq_tsum_one_div_nat_cpow, MellinConvergent.div_const, AddChar.sum_apply_eq_zero_iff_ne_zero, ProbabilityTheory.analyticAt_complexMGF, AnalyticOn.clog, HurwitzZeta.hurwitzEvenFEPair_zero_symm, UnitAddTorus.coeFn_mFourierLp, circleIntegral.integral_sub_zpow_of_undef, PeriodPair.weierstrassPExcept_eq_tsum, TemperedDistribution.fourierMultiplierCLM_apply, HasDerivWithinAt.complexToReal_fderiv, Real.tsum_eq_tsum_fourier_of_rpow_decay_of_summable, TemperedDistribution.fourier_toTemperedDistributionCLM_eq, ContDiffOn.ccos, hasSum_ofReal, ofRealCLM_nnnorm, imCLM_norm, AnalyticOnNhd.clog, intervalIntegral.intervalIntegrable_cpow, integral_exp_mul_I_eq_sinc, PeriodPair.differentiableOn_derivWeierstrassP, PeriodPair.weierstrassPExcept_def, TemperedDistribution.fourierMultiplierCLM_const, PeriodPair.meromorphic_derivWeierstrassP, HurwitzZeta.hasSum_int_cosZeta, hasSum_jacobiTheta₂_term_fderiv, NumberField.mixedEmbedding.mem_span_latticeBasis, TemperedDistribution.fourierTransformInv_toTemperedDistributionCLM_eq, analyticOnNhd_sin, hasSum_sin, ValueDistribution.proximity_mul_zero_le, Orientation.kahler_neg_orientation, HasFDerivWithinAt.cexp, EisensteinSeries.D2_inv, EisensteinSeries.hasSum_e2Summand_symmetricIco, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, conjCLE_toLinearEquiv, HasDerivAt.complexToReal_fderiv', SlashInvariantForm.slash_action_generators, hasSum_jacobiTheta₂'_term, NumberField.mixedEmbedding.negAt_apply_isReal_and_notMem, SchwartzMap.toTemperedDistributionCLM_apply_apply, EisensteinSeries.q_expansion_riemannZeta, HasDerivAt.complexToReal_fderiv, integral_exp_mul_I_eq_sin, integral_boundary_rect_of_hasFDerivAt_real_off_countable, MeasureTheory.SignedMeasure.re_toComplexMeasure, TemperedDistribution.smulLeftCLM_sub, one_add_cpow_hasFPowerSeriesAt_zero, HurwitzZeta.hasSum_nat_cosZeta, NumberField.mixedEmbedding.covolume_idealLattice, NumberField.mixedEmbedding.volume_preserving_negAt, OnePoint.isZeroAt_iff_forall_SL2Z, hasSum_cauchyPowerSeries_integral, LinearMap.coe_complexOfReal, UpperHalfPlane.contMDiff_num, UpperHalfPlane.mdifferentiable_denom, ContDiffWithinAt.ccos, angle_eq_abs_arg, Function.locallyFinsuppWithin.toClosedBall_divisor, LSeries.term_convolution, NumberField.mixedEmbedding.negAt_apply_isComplex, hasFDerivAt_cpow, ProbabilityTheory.isGaussian_iff_charFun_eq, OnePoint.isBoundedAt_iff, convex_halfSpace_im_lt, Polynomial.rootSet_derivative_subset_convexHull_rootSet, HasFDerivAt.cexp, NumberField.mixedEmbedding.normAtComplexPlaces_normAtAllPlaces, LSeriesSummable.sum, HurwitzZeta.hasSum_expZeta_of_one_lt_re, eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet, OnePoint.IsZeroAt.smul_iff, HurwitzZeta.hasSum_int_completedHurwitzZetaOdd, UpperHalfPlane.smulFDeriv_J_mul, PeriodPair.summable_weierstrassPSummand, one_div_sub_sq_hasFPowerSeriesOnBall_zero, DirichletCharacter.summable_neg_log_one_sub_mul_prime_cpow, EisensteinSeries.linear_left_summable, PeriodPair.hasSumLocallyUniformly_weierstrassPExcept, ofRealCLM_apply, cfcHom_real_eq_restrict, NumberField.mixedEmbedding.mem_negAt_plusPart_of_mem, ValueDistribution.characteristic_sub_characteristic_inv_le, IsSelfAdjoint.spectrumRestricts, eqOn_iteratedDeriv_cotTerm, tsum_riemannZetaSummand, restrictScalars_one_smulRight, summable_ofReal, one_div_one_sub_pow_hasFPowerSeriesOnBall_zero, AnalyticAt.harmonicAt_conj, MeasureTheory.integral_charFun_Icc, ZMod.completedLFunction_eq, UnitAddTorus.orthonormal_mFourier, dist_of_im_eq, AnalyticOnNhd.cexp, EulerSine.integral_sin_mul_sin_mul_cos_pow_eq, analyticOnNhd_cexp, MDifferentiable.slash, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_mem_fundamentalCone_iff, fourierCoeff_toLp, ProbabilityTheory.hasDerivAt_complexMGF, ProbabilityTheory.IsGaussian.charFunDual_eq, coe_fourierBasis, tsum_exp_neg_quadratic, ModularFormClass.qExpansion_coeff, CuspForm.coe_translate, PeriodPair.derivWeierstrassP_sub_coe, isAddQuotientCoveringMap_exp, hasSum_sq_fourierCoeffOn, SpectrumRestricts.real_iff, torusIntegral_const_mul, cosh_eq_tsum, NumberField.mixedEmbedding.volume_preserving_mixedSpaceToRealMixedSpace_symm, integral_exp_neg_mul_rpow, contDiff_exp, TemperedDistribution.fourierMultiplierCLM_toTemperedDistributionCLM_eq, nndist_of_re_eq, hasSum_mellin_pi_mul, le_radius_cauchyPowerSeries, HurwitzZeta.hasSum_int_sinKernel, qExpansion_sub, hasMellin_one_Ioc, ValueDistribution.proximity_mul_top_le, QuasispectrumRestricts.real_iff, TemperedDistribution.instLineDerivSMulReal, cot_series_rep, Summable.clog_one_sub, MeasureTheory.Measure.toTemperedDistribution_apply, analyticOn_iff_differentiableOn, ContDiffAt.harmonicAt, ValueDistribution.characteristic_mul_zero_eventuallyLE, EisensteinSeries.isBoundedAtImInfty_eisensteinSeries_SIF, ValueDistribution.characteristic_pow_zero, ValueDistribution.characteristic_top_mul_le, ContDiff.ccosh, abel_aux, norm_sub_le_angle, PeriodPair.weierstrassP_add_coe, NumberField.mixedEmbedding.stdBasis_apply_isComplex_fst, ContDiffAt.ccosh, TemperedDistribution.fourier_lineDerivOp_eq, TemperedDistribution.fourier_delta_zero, PeriodPair.order_weierstrassP, PeriodPair.instProperSpaceSubtypeComplexMemSubmoduleIntLattice, volume_sum_rpow_lt, conjCLE_coe_toLinearMap, analyticOn_cos, ModularForm.coeHom_apply, MeromorphicNFOn.Gamma, hasDerivAt_logTaylor, iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow, ModularForm.slash_action_eq'_iff, HarmonicAt.analyticAt, lintegral_comp_polarCoord_symm, NumberField.mixedEmbedding.fundamentalDomain_stdBasis, ValueDistribution.characteristic_sub_characteristic_inv, NumberField.mixedEmbedding.span_latticeBasis, UnitAddTorus.instContinuousSMulComplexSubtypeAEEqFunVolumeMemAddSubgroupLp, integral_cexp_quadratic, TemperedDistribution.lineDerivOp_toTemperedDistributionCLM_eq, isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts, orthonormalBasisOneI_repr_symm_apply, UnitAddTorus.hasSum_mFourier_series_L2, dist_eq, TemperedDistribution.laplacian_eq_sum, NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul, ValueDistribution.isBigO_characteristic_sub_characteristic_inv, MeasureTheory.ComplexMeasure.HaveLebesgueDecomposition.rePart, iteratedDeriv_add_one_sinh, TemperedDistribution.instContinuousLineDeriv, iteratedDeriv_even_cos, iteratedDeriv_add_one_sin, volume_preserving_equiv_real_prod, NumberField.mixedEmbedding.fundamentalCone.norm_normAtAllPlaces, ZMod.LFunction_def_even, one_div_sub_pow_hasFPowerSeriesOnBall_zero, ContDiffWithinAt.ccosh, HadamardThreeLines.diffContOnCl_interpStrip, angle_div_left_eq_angle_mul_right, HurwitzZeta.hasSum_nat_completedSinZeta, Distribution.IsVanishingOn.iteratedLineDerivOp, LSeries_eq_mul_integral, hasFPowerSeriesOn_cauchy_integral, UpperHalfPlane.contMDiff_denom_zpow, circleIntegral_div_sub_of_differentiable_on_off_countable, contDiffOn_tsum_cexp, convex_halfSpace_re_ge, PeriodPair.latticeBasis_one, DifferentiableOn.hasFPowerSeriesOnBall, analyticAt_sinh, NumberField.mixedEmbedding.covolume_integerLattice, Orientation.kahler_apply_self, PeriodPair.weierstrassP_sub_coe, analyticOn_univ_iff_differentiable, conjCLE_nnorm, HasStrictDerivAt.complexToReal_fderiv', fourierIntegral_gaussian_innerProductSpace, Differentiable.contDiff, iteratedDeriv_add_one_cos, MeasureTheory.SignedMeasure.toComplexMeasure_apply_re, HurwitzZeta.hurwitzOddFEPair_f₀, EisensteinSeries.qExpansion_identity_pnat, UpperHalfPlane.petersson_slash_SL, Orientation.kahler_rotation_left', zeta_eq_tsum_one_div_nat_add_one_cpow, ValueDistribution.characteristic_mul_zero_le, NumberField.mixedEmbedding.euclidean.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, Distribution.dsupport_smulLeftCLM_subset, convex_halfSpace_im_ge, angle_le_mul_norm_sub, nnnorm_ofNat, cot_pi_mul_contDiffWithinAt, ModularForm.SL_slash_def, PeriodPair.hasSum_weierstrassP, convex_halfSpace_re_lt, NumberField.mixedEmbedding.euclidean.instIsZLatticeRealMixedSpaceIntegerLattice, TemperedDistribution.smulLeftCLM_add, PeriodPair.coeff_weierstrassPSeries, PeriodPair.isOpen_compl_lattice_diff, restrictScalars_toSpanSingleton, Orientation.normSq_kahler, volume_closedBall, nnnorm_nnratCast, hasSum_cos', PeriodPair.derivWeierstrassP_coe, locallyFinsuppWithin.logCounting_divisor, NumberField.mixedEmbedding.negAt_symm, MeasureTheory.iteratedDeriv_charFun, fourierSubalgebra_coe, AnalyticAt.harmonicAt_re, contDiffAt_tan, HurwitzZeta.hurwitzOddFEPair_ε, analyticWithinAt_sinh, analyticOnNhd_cosh, exp_sub_sum_range_succ_isLittleO_pow, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIntegerLattice, MeasureTheory.measureReal_abs_gt_le_integral_charFun, NumberField.mixedEmbedding.negAt_apply_isReal_and_mem, hasFDerivAt_jacobiTheta₂, ContDiffWithinAt.csin, NumberField.mixedEmbedding.volume_negAt_plusPart, NumberField.mixedEmbedding.convexBodyLT'_volume, OnePoint.IsBoundedAt.smul_iff, ContDiffAt.ccos, TemperedDistribution.fourierTransform_apply, MeromorphicOn.circleAverage_log_norm, contDiff_sinh, tendsto_logDeriv_euler_cot_sub, SlashInvariantForm.coe_trace, isConformalMap_complex_linear_conj, NumberField.mixedEmbedding.iUnion_negAt_plusPart_union, exp_sub_sum_range_isBigO_pow, EisensteinSeries.summable_linear_sub_mul_linear_add, hasSum_mellin_pi_mul₀, ValueDistribution.characteristic_pow_top, MeasureTheory.measureReal_abs_dual_gt_le_integral_charFunDual, Orientation.kahler_rightAngleRotation_left, UnitAddTorus.hasSum_mFourier_series_of_summable, Orientation.kahler_comp_linearIsometryEquiv, HurwitzZeta.hasSum_nat_hurwitzZetaOdd, cfcₙHom_real_eq_restrict, PeriodPair.latticeEquiv_symm_apply, PeriodPair.hasFPowerSeriesOnBall_weierstrassP, MeasureTheory.ComplexMeasure.im_apply, Function.locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const, betaIntegral_convergent, EisensteinSeries.tsum_tsum_symmetricIco_sub_eq, enorm_exp_I_mul_ofReal, NumberField.canonicalEmbedding.mem_rat_span_latticeBasis, harmonic_is_realOfHolomorphic, PeriodPair.hasSumLocallyUniformly_derivWeierstrassPExcept, ModularForm.summable_logDeriv_one_sub_eta_q, PeriodPair.weierstrassPSeries_hasSum, LSeries_sum, analyticOn_cexp, span_fourierLp_closure_eq_top, circleIntegral.integral_sub_zpow_of_ne, Orientation.kahler_rotation_left, LindemannWeierstrass.integral_exp_mul_eval, ModularFormClass.hasSum_qExpansion_of_abs_lt, LSeries.iteratedDeriv_alternating, conjCLE_enorm, AnalyticAt.cpow, hasSum_conj, UpperHalfPlane.meromorphicOrderAt_comp_smul, re_tsum, EisensteinSeries.q_expansion_bernoulli, circleIntegral.integral_smul_const, NumberField.mixedEmbedding.volume_eq_two_pow_mul_two_pi_pow_mul_integral, InnerProductSpace.laplacian_eq_iteratedFDeriv_complexPlane, NumberField.mixedEmbedding.injective_mixedSpaceOfRealSpace, SchwartzMap.integral_fourier_mul_eq, volume_preserving_equiv_pi, norm_sub_one_sq_eqOn_sphere, PeriodPair.hasFPowerSeriesOnBall_derivWeierstrassPExcept, ValueDistribution.proximity_zero_of_complexValued, tsum_dirichletSummand, EulerSine.tendsto_integral_cos_pow_mul_div, circleIntegrable_sub_zpow_iff, Polynomial.fourierCoeff_toAddCircle_natCast, conjCLE_apply, nnnorm_natCast, fourierCoeffOn_of_hasDerivAt_Ioo, NumberField.mixedEmbedding.volume_eq_zero, nndist_conj_self, MeasureTheory.taylorWithinEval_charFun_two_zero, NumberField.mixedEmbedding.stdBasis_apply_isReal, DirichletCharacter.LSeries_eulerProduct_exp_log, NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, ValueDistribution.characteristic_zero_mul_eventually_le, MeasureTheory.ComplexMeasure.equivSignedMeasureₗ_symm_apply, PeriodPair.analyticOnNhd_derivWeierstrassP, GaussianFourier.integral_cexp_neg_mul_sq_add_real_mul_I, SlashInvariantForm.slash_action_generators_SL2Z, NumberField.mixedEmbedding.convexBodyLT_convex, hasFPowerSeriesOnBall_cuspFunction, Orientation.kahler_mul, GaussianFourier.integral_cexp_neg_mul_sum_add, tsum_sq_fourierCoeffOn, ModularFormClass.qExpansion_coeff_eq_circleIntegral, ProbabilityTheory.isGaussian_iff_charFunDual_eq, one_div_one_sub_cpow_hasFPowerSeriesOnBall_zero, fourierIntegral_gaussian, ArithmeticFunction.vonMangoldt.LSeries_residueClass_eq, PeriodPair.meromorphic_weierstrassP, EisensteinSeries.tendsto_double_sum_S_act, TemperedDistribution.fourierMultiplierCLM_apply_apply, analyticOnNhd_canonicalFactor, sinh_eq_tsum, HurwitzZeta.hasSum_nat_hurwitzZetaEven_of_mem_Icc, NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIdealLattice, PeriodPair.analyticAt_derivWeierstrassPExcept, NumberField.mixedEmbedding.fundamentalCone.logMap_expMap, MeasureTheory.ProbabilityMeasure.tendsto_charPoly_of_tendsto_charFun, TemperedDistribution.instFourierInvSMul, Derivative.normalizedDerivOfComplex_mdifferentiable, imCLM_coe, integral_gaussian_sq_complex, HurwitzZeta.hurwitzOddFEPair_g₀, meromorphicNFOn_canonicalFactor, ModularForm.discriminant_T_invariant, PeriodPair.instDiscreteTopologySubtypeComplexMemSubmoduleIntLattice, Distribution.dsupport_iteratedLineDerivOp_subset, Orientation.kahler_map, TemperedDistribution.instFourierInvAdd, EisensteinSeries.summable_e2Summand_symmetricIcc, UnitAddTorus.hasSum_prod_mFourierCoeff, NumberField.mixedEmbedding.latticeBasis_apply, circleIntegral.circleIntegral_congr_codiscreteWithin, BoundedContinuousFunction.star_mem_range_charAlgHom, TemperedDistribution.fourierInv_apply, AnalyticAt.harmonicAt_log_norm, MeasureTheory.contDiff_charFun, sin_eq_tsum, HurwitzZeta.hurwitzOddFEPair_f, fourierCoeff.const_mul, AnalyticOnNhd.sum_divisor_le, MeasureTheory.measureReal_abs_inner_gt_le_integral_charFun, Real.tsum_eq_tsum_fourier_of_rpow_decay, SlashInvariantForm.slash_S_apply, TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq, one_add_cpow_hasFPowerSeriesOnBall_zero, hasSum_conj', TemperedDistribution.instLineDerivAdd, hasSum_fourier_series_of_summable, GammaSeq_eq_approx_Gamma_integral, hasSum_taylorSeries_neg_log, nnnorm_exp_ofReal_mul_I, PeriodPair.hasSumLocallyUniformly_aux, NumberField.mixedEmbedding.commMap_apply_of_isReal, integral_boundary_rect_of_continuousOn_of_hasFDerivAt_real, TemperedDistribution.instLineDerivSMulComplex, LSeries_analyticOn, iteratedDeriv_odd_cos, ValueDistribution.characteristic_zero_mul_le, Function.Complex.hasTemperateGrowth_ofReal, log_eq_integral, equivRealProdCLM_symm_apply_re, one_div_one_sub_sq_hasFPowerSeriesOnBall_zero, NumberField.mixedEmbedding.latticeBasis_repr_apply, dist_mk, SchwartzMap.integral_fourierInv_mul_eq, TemperedDistribution.laplacian_toTemperedDistributionCLM_eq, summable_one_div_nat_cpow, logDeriv_prod_sineTerm_eq_sum_cotTerm, ValueDistribution.proximity_pow_top, summable_prod_eisSummand, mdifferentiable_jacobiTheta, NumberField.mixedEmbedding.normAtPlace_negAt, Distribution.dsupport_lineDerivOp_subset, PeriodPair.hasFPowerSeriesOnBall_weierstrassPExcept, EisensteinSeries.G2_eq_tsum_cexp, sameRay_iff, TemperedDistribution.fourierMultiplierCLM_sum, PeriodPair.hasSum_weierstrassPExcept, ProbabilityTheory.hasDerivAt_iteratedDeriv_complexMGF, NumberField.mixedEmbedding.finrank, SchwartzMap.integral_fourier_smul_eq, imCLM_nnnorm, HurwitzZeta.hurwitzOddFEPair_k, EisensteinSeries.qExpansion_identity, iteratedDeriv_even_sin, UpperHalfPlane.contMDiffAt_ofComplex, fourierSubalgebra_closure_eq_top, ModularForm.prod_fintype_slash, GaussianFourier.integral_cexp_neg_sum_mul_add, NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply, circleIntegrable_sub_inv_iff, sameRay_iff_arg_div_eq_zero, ModularForm.holo', tsum_eisSummand_eq_tsum_sigma_mul_cexp_pow, starConvex_slitPlane, ProbabilityTheory.analyticOn_complexMGF, integral_rpow_mul_exp_neg_mul_rpow, ModularForm.discriminant_S_invariant, NumberField.mixedEmbedding.negAt_apply_norm_isReal, angle_one_left, HurwitzZeta.hasSum_int_sinZeta, iteratedDeriv_even_sinh, iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum, summable_log_one_add_of_summable, ArithmeticFunction.LSeries_zeta_eulerProduct_exp_log, ModularFormClass.hasSum_qExpansion_of_norm_lt, volume_ball, TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq, DifferentiableOn.analyticOnNhd, ModularFormClass.bdd_at_infty_slash, jacobiTheta_eq_tsum_nat, hasSum_sq_fourierCoeff, differentiable_iteratedDeriv_sinh, LSeries.term_sum_apply, ContDiffAt.cexp, UpperHalfPlane.contMDiffAt_iff, Orientation.kahler_apply_apply, InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_univ_re_eq, UpperHalfPlane.instIsManifoldComplexModelWithCornersSelfTopWithTopENat, taylorSeries_eq_on_eball', UnitAddTorus.mFourierBasis_repr, angle_one_right, ModularForm.slash_def, Function.Periodic.contDiff_qParam, MeasureTheory.ComplexMeasure.absolutelyContinuous_ennreal_iff, PeriodPair.differentiableOn_weierstrassPExcept, analyticOnNhd_iff_differentiableOn, conjCLE_norm, MeasureTheory.Lp.ker_toTemperedDistributionCLM_eq_bot, MeasureTheory.Lp.toTemperedDistribution_toLp_eq, ContDiffAt.csinh, fourierBasis_repr, PeriodPair.derivWeierstrassPExcept_add_coe, ValueDistribution.logCounting_zero_sub_logCounting_top_eq_circleAverage_sub_const, analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt, MeasureTheory.taylorWithinEval_charFun_two_zero', iteratedDeriv_add_one_cosh, CuspFormClass.zero_at_infty_slash, ContDiff.csinh, PeriodPair.differentiableOn_weierstrassP, UnitAddTorus.span_mFourier_closure_eq_top, TemperedDistribution.laplacian_apply_apply, ModularForm.is_invariant_one', imCLM_enorm, TemperedDistribution.smulLeftCLM_smulLeftCLM_apply, EisensteinSeries.tendsto_tsum_one_div_linear_sub_succ_eq, UpperHalfPlane.mdifferentiable_coe, TemperedDistribution.isVanishingOn_delta, integral_complex_ofReal, summable_cotTerm, PeriodPair.weierstrassPExceptSeries_hasSum, Orientation.kahler_rotation_right, ofRealCLM_enorm, integral_Ioi_cpow_of_lt, ModularFormClass.analyticAt_cuspFunction_zero, HadamardThreeLines.scale_diffContOnCl, NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis, TemperedDistribution.lineDerivOp_apply_apply, HadamardThreeLines.diffContOnCl_invInterpStrip, MeasureTheory.ComplexMeasure.re_apply, intervalIntegral.intervalIntegrable_cpow', UnitAddTorus.hasSum_mFourier_series_apply_of_summable, UnitAddTorus.hasSum_sq_mFourierCoeff, TemperedDistribution.lineDerivOp_fourierInv_eq, hasSum_taylorSeries_log, HurwitzZeta.hurwitzOddFEPair_g, circleTransformDeriv_bound, PeriodPair.hasSum_sumInvPow, hasFPowerSeriesOnBall_of_differentiable_off_countable, lintegral_comp_pi_polarCoord_symm, EisensteinSeries.eisensteinSeries_tendstoLocallyUniformlyOn, analyticWithinAt_sin, conformalAt_iff_differentiableAt_or_differentiableAt_comp_conj, AnalyticAt.harmonicAt, analyticAt_clog, LSeriesHasSum.sum, ProbabilityTheory.IsGaussian.charFun_eq, equivRealProdCLM_symm_apply_im, integral_gaussian_complex, complexOfReal_hasDerivAt, Real.hasFDerivAt_fourierChar_neg_bilinear_right, InnerProductSpace.harmonic_is_realOfHolomorphic_univ, summable_bernoulli_fourier, PeriodPair.periodic_weierstrassP, SchwartzMap.integral_inner_fourier_fourier, ModularFormClass.holo, EisensteinSeries.summable_e2Summand_symmetricIco, GaussianFourier.integrable_cexp_neg_sum_mul_add, hasSum_sinh, integral_exp_mul_complex_Iic, circleIntegral.integral_sub_center_inv, MeasureTheory.Lp.toTemperedDistribution_apply, TemperedDistribution.smulLeftCLM_const, iteratedDeriv_cexp_const_mul, hasStrictFDerivAt_log_real, TemperedDistribution.smulLeftCLM_sum, EisensteinSeries.summable_right_one_div_linear_sub_one_div_linear_succ, hasSum_sin', jacobiTheta₂_fderiv_undef, NumberField.mixedEmbedding.euclidean.finrank, EisensteinSeries.summable_linear_right_add_one_mul_linear_right, ModularForm.is_invariant_const, nnnorm_I, fourierCoeff_liftIoc_eq, volume_sum_rpow_lt_one, betaIntegral_convergent_left, hasSum_one_div_pow_mul_fourier_mul_bernoulliFun, TemperedDistribution.instContinuousFourierInv, NumberField.mixedEmbedding.measurableSet_negAt_plusPart, MeasureTheory.SignedMeasure.toComplexMeasure_apply_im, sin_eq_tsum', one_add_cpow_hasFPowerSeriesOnBall_zero, reCLM_norm, ValueDistribution.proximity_top_mul_le, ModularForm.SL_slash_apply, ContDiffWithinAt.csinh, ZMod.LFunction_residue_one, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, NumberField.mixedEmbedding.convexBodySum_convex, PeriodPair.mul_ω₁_add_mul_ω₂_mem_lattice, convex_halfSpace_im_le, MeasureTheory.ComplexMeasure.toComplexMeasure_to_signedMeasure, NumberField.mixedEmbedding.fundamentalCone.volume_normLeOne, TemperedDistribution.fourier_apply, ContinuousLinearMap.coe_complexOfReal, hasMellin_cpow_Ioc, EisensteinSeries.eisensteinSeries_SIF_MDifferentiable, tsum_sq_fourierCoeff, VectorFourier.integral_fourierIntegral_smul_eq_flip, differentiable_iteratedDeriv_cos, SchwartzMap.coe_apply, integral_mul_cpow_one_add_sq, DifferentiableOn.analyticAt, ofReal_tsum, MeasureTheory.ComplexMeasure.equivSignedMeasureₗ_apply, AddChar.coe_complexBasis, AnalyticWithinAt.clog, DifferentiableAt.conformalAt, one_div_one_sub_hasFPowerSeriesOnBall_zero, UpperHalfPlane.mdifferentiableAt_iff, edist_of_re_eq, rightAngleRotation, fourierCoeffOn_of_hasDerivAt, UpperHalfPlane.IsZeroAtImInfty.slash, PeriodPair.analyticOnNhd_weierstrassPExcept, DiffContOnCl.hasFPowerSeriesOnBall, TemperedDistribution.smulLeftCLM_smul, analyticAt_cos, analyticOnNhd_cos, imCLM_apply, ArithmeticFunction.iteratedDeriv_LSeries_alternating, NumberField.mixedEmbedding.normAtAllPlaces_mixedSpaceOfRealSpace, PeriodPair.indep, isConformalMap_complex_linear, Real.tsum_eq_tsum_fourierIntegral, ModularForm.coe_translate, SchwartzMap.tsum_eq_tsum_fourierIntegral, analyticWithinAt_cexp, Orientation.kahler_rightAngleRotation_right, MeasureTheory.intervalIntegrable_charFun, hasSum_arctan, MeasureTheory.charFun_eq_integral_innerProbChar, edist_of_im_eq, ValueDistribution.characteristic_top_mul_eventually_le, iteratedDeriv_odd_cosh, contDiff_sin, TemperedDistribution.derivCLM_apply_apply, HurwitzZeta.hasSum_int_completedCosZeta, NumberField.mixedEmbedding.volume_eq_two_pi_pow_mul_integral, contDiff_cos, hasSum_cosh, Orientation.norm_kahler, NumberField.mixedEmbedding.disjoint_span_commMap_ker, taylorSeries_eq_of_entire', conj_tsum, PeriodPair.summable_weierstrassPExceptSummand, Meromorphic.Gamma, ModularForm.coe_trace, InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq, HasStrictDerivAt.complexToReal_fderiv, convex_halfSpace_re_gt, enorm_exp_ofReal_mul_I, AddChar.complexBasis_apply, ProbabilityTheory.analyticOnNhd_complexMGF, NumberField.mixedEmbedding.convexBodySum_volume, AnalyticAt.cexp', SlashInvariantForm.coeHom_injective, EisensteinSeries.eisensteinSeries_slash_apply, TemperedDistribution.fourierTransformInv_apply, hasSum_cos, ModularFormClass.qExpansionFormalMultilinearSeries_coeff, UpperHalfPlane.contMDiff_smul, HurwitzZeta.hasSum_int_completedSinZeta, eqOn_iteratedDerivWithin_cotTerm_integerComplement, zeta_nat_eq_tsum_of_gt_one, HurwitzZeta.hasSum_nat_hurwitzZetaOdd_of_mem_Icc, AddChar.expect_apply_eq_ite, reCLM_enorm, UpperHalfPlane.contMDiff_denom, nnnorm_real, BoundedContinuousFunction.separatesPoints_charPoly, one_div_sub_sq_sub_one_div_sq_hasFPowerSeriesOnBall_zero, PeriodPair.lattice_eq_span_range_basis, NumberField.mixedEmbedding.integral_comp_polarCoord_symm, E2_mdifferentiable, EisensteinSeries.eisensteinSeriesSIF_mdifferentiable, PeriodPair.ω₁_mem_lattice, log_inv_eq_integral, OnePoint.isZeroAt_iff, UnitAddTorus.span_mFourierLp_closure_eq_top, ZMod.LFunction_dft, ContDiffOn.cexp, PeriodPair.analyticOnNhd_weierstrassP, HurwitzZeta.hasSum_int_completedHurwitzZetaEven, ContDiff.csin, UpperHalfPlane.mdifferentiable_denom_zpow, Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay, MeromorphicOn.Gamma, integral_cpow_mul_exp_neg_mul_Ioi, dist_of_re_eq, NumberField.mixedEmbedding.commMap_canonical_eq_mixed, SlashInvariantFormClass.slash_action_eq, integral_cos_mul_complex, ContDiffOn.csinh, Polynomial.fourierCoeff_toAddCircle, hasFPowerSeriesOnBall_ofScalars_mul_add_zero, hasSum_iff, NumberField.mixedEmbedding.norm_negAt, SlashInvariantForm.slash_action_eqn, TemperedDistribution.lineDeriv_eq_fourierMultiplierCLM, summable_pow_mul_cexp, ModularFormClass.hasSum_qExpansion, ModularFormClass.qExpansion_coeff_eq_intervalIntegral, approx_Gamma_integral_tendsto_Gamma_integral, tendsto_tsum_powerSeries_nhdsWithin_stolzSet, summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp, Derivative.serreDerivative_mdifferentiable, isConformalMap_iff_is_complex_or_conj_linear, PeriodPair.ω₂_mem_lattice, summable_jacobiTheta₂'_term_iff, UpperHalfPlane.mdifferentiable_iff, analyticAt_iff_eventually_differentiableAt, fourierCoeffOn_of_hasDeriv_right, analyticOnNhd_sinh, analyticWithinAt_cos, NumberField.mixedEmbedding.normAtPlace_mixedSpaceOfRealSpace, ModularForm.is_invariant_one, PeriodPair.derivWeierstrassPExcept_def, EisensteinSeries.tsum_symmetricIco_tsum_eq_S_act, Distribution.IsVanishingOn.lineDerivOp, UpperHalfPlane.mdifferentiableAt_ofComplex, LSeries_eq_mul_integral', AnalyticAt.cexp, Summable.hasSumUniformlyOn_log_one_add, fourier_gaussian_pi, Real.fourier_smul_convolution_eq, dist_conj_self, EisensteinSeries.D2_mul, TemperedDistribution.laplacianCLM_apply, ValueDistribution.proximity_sub_proximity_inv_eq_circleAverage, continuousAt_gaussian_integral, im_tsum, coeFn_fourierLp, taylorSeries_eq_on_emetric_ball', fourierCoeff_liftIco_eq, NumberField.mixedEmbedding.disjoint_negAt_plusPart, NumberField.mixedEmbedding.volume_fundamentalDomain_stdBasis, PositiveLinearMap.preGNS_norm_sq, EulerSine.integral_cos_mul_cos_pow_even, circleIntegral.integral_const_mul, MeasureTheory.Lp.toTemperedDistribution_smul_eq, UpperHalfPlane.IsBoundedAtImInfty.slash, Differentiable.analyticAt, equivRealProdCLM_apply, NumberField.mixedEmbedding.volume_eq_two_pow_mul_volume_plusPart, ValueDistribution.characteristic_mul_top_eventuallyLE, MeasureTheory.charFun_eq_integral_probChar, one_div_sub_hasFPowerSeriesOnBall_zero, EulerProduct.exp_tsum_primes_log_eq_tsum, fourierIntegral_gaussian_pi', tendsto_tsum_powerSeries_nhdsWithin_lt, PeriodPair.finrank_lattice, PeriodPair.derivWeierstrassP_add_coe, integral_gaussian_complex_Ioi, ModularForm.SL_smul_slash, NumberField.mixedEmbedding.convexBodyLT'_convex, TemperedDistribution.smulLeftCLM_apply_apply, summable_jacobiTheta₂_term_iff, NumberField.mixedEmbedding.mem_rat_span_latticeBasis, hasSum_mellin_pi_mul_sq, EisensteinSeries.eisensteinSeries_tendstoLocallyUniformly, BoundedContinuousFunction.char_mem_charPoly, MeasureTheory.SignedMeasure.im_toComplexMeasure, NumberField.mixedEmbedding.fundamentalCone.logMap_normAtAllPlaces, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne, rotation, differentiableAt_iteratedDerivWithin_cexp, pi_mul_cot_pi_q_exp, PeriodPair.weierstrassPExcept_add, SchwartzMap.tsum_eq_tsum_fourier, NumberField.mixedEmbedding.normAtAllPlaces_normAtAllPlaces, norm_jacobiTheta₂_term_fderiv_le, MeasureTheory.taylorWithinEval_charFun_zero, EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF, PeriodPair.instIsZLatticeRealComplexLattice, Summable.tendstoUniformlyOn_tsum_nat_log_one_add, UpperHalfPlane.mdifferentiable_smul, dist_eq_re_im, ModularForm.slash_apply, angle_exp_exp, AnalyticOn.cexp, restrictScalars_toSpanSingleton', Polynomial.fourierCoeff_toAddCircle_eq_zero_of_lt_zero, differentiable_iteratedDeriv_cosh, rectangle_eq_convexHull, NumberField.mixedEmbedding.mixedSpaceOfRealSpace_apply, analyticAt_cexp, EisensteinSeries.G2_T_transform, reCLM_apply, NumberField.mixedEmbedding.lintegral_comp_polarSpaceCoord_symm, PeriodPair.differentiableOn_derivWeierstrassPExcept, UpperHalfPlane.petersson_slash, DifferentiableOn.analyticOn, EisensteinSeries.tsum_symmetricIco_tsum_sub_eq, fourierCoeff_fourier
limAux 📖	CompOp	1 math math: equiv_limAux

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_im_div_norm_le_one 📖	mathematical	—	Real Real.instLE abs Real.lattice Real.instAddGroup DivInvMonoid.toDiv Real.instDivInvMonoid im Norm.norm Complex instNorm Real.instOne	—	norm_zero div_zero abs_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass abs_div Real.instIsStrictOrderedRing abs_norm div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono norm_pos_iff one_mul
abs_im_eq_norm 📖	mathematical	—	abs Real Real.lattice Real.instAddGroup im Norm.norm Complex instNorm re Real.instZero	—	not_iff_not LE.le.lt_iff_ne abs_im_le_norm abs_im_lt_norm
abs_im_le_norm 📖	mathematical	—	Real Real.instLE abs Real.lattice Real.instAddGroup im Norm.norm Complex instNorm	—	Real.abs_le_sqrt normSq_apply sq le_add_of_nonneg_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono Real.instIsOrderedRing
abs_im_lt_norm 📖	mathematical	—	Real Real.instLT abs Real.lattice Real.instAddGroup im Norm.norm Complex instNorm	—	MulZeroClass.mul_zero mul_one zero_sub abs_neg norm_mul norm_I add_zero abs_re_lt_norm
abs_re_div_norm_le_one 📖	mathematical	—	Real Real.instLE abs Real.lattice Real.instAddGroup DivInvMonoid.toDiv Real.instDivInvMonoid re Norm.norm Complex instNorm Real.instOne	—	norm_zero div_zero abs_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass abs_div Real.instIsStrictOrderedRing abs_norm div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono norm_pos_iff one_mul
abs_re_eq_norm 📖	mathematical	—	abs Real Real.lattice Real.instAddGroup re Norm.norm Complex instNorm im Real.instZero	—	not_iff_not LE.le.lt_iff_ne abs_re_le_norm abs_re_lt_norm
abs_re_le_norm 📖	mathematical	—	Real Real.instLE abs Real.lattice Real.instAddGroup re Norm.norm Complex instNorm	—	mul_self_le_mul_self_iff IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Real.instIsOrderedRing abs_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add norm_nonneg abs_mul_abs_self norm_mul_self_eq_normSq re_sq_le_normSq
abs_re_lt_norm 📖	mathematical	—	Real Real.instLT abs Real.lattice Real.instAddGroup re Norm.norm Complex instNorm	—	norm_def Real.lt_sqrt abs_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add normSq_apply sq_abs sq lt_add_iff_pos_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le mul_self_pos AddGroup.existsAddOfLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsStrictOrderedRing.toMulPosStrictMono
dist_conj_self 📖	mathematical	—	Dist.dist Complex PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing Real Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat abs Real.lattice Real.instAddGroup im	—	Nat.instAtLeastTwoHAddOfNat dist_of_re_eq conj_re conj_im dist_comm Real.dist_eq sub_neg_eq_add two_mul abs_mul Real.instIsOrderedRing abs_of_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid zero_lt_two' Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing
dist_eq 📖	mathematical	—	Dist.dist Complex PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup Norm.norm instNorm instSub	—	dist_eq_norm
dist_eq_re_im 📖	mathematical	—	Dist.dist Complex PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup Real.sqrt Real Real.instAdd Monoid.toPow Real.instMonoid Real.instSub re im	—	sq dist_eq
dist_mk 📖	mathematical	—	Dist.dist Complex PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup Real.sqrt Real Real.instAdd Monoid.toPow Real.instMonoid Real.instSub	—	dist_eq_re_im
dist_of_im_eq 📖	mathematical	im	Dist.dist Complex PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup Real Real.pseudoMetricSpace re	—	dist_eq_re_im sub_self zero_pow two_ne_zero add_zero Real.sqrt_sq_eq_abs Real.dist_eq
dist_of_re_eq 📖	mathematical	re	Dist.dist Complex PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup Real Real.pseudoMetricSpace im	—	dist_eq_re_im sub_self zero_pow two_ne_zero zero_add Real.sqrt_sq_eq_abs Real.dist_eq
dist_self_conj 📖	mathematical	—	Dist.dist Complex PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing Real Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat abs Real.lattice Real.instAddGroup im	—	Nat.instAtLeastTwoHAddOfNat dist_comm dist_conj_self
edist_of_im_eq 📖	mathematical	im	EDist.edist Complex PseudoEMetricSpace.toEDist EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace instNormedAddCommGroup Real Real.metricSpace re	—	edist_nndist nndist_of_im_eq
edist_of_re_eq 📖	mathematical	re	EDist.edist Complex PseudoEMetricSpace.toEDist EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace instNormedAddCommGroup Real Real.metricSpace im	—	edist_nndist nndist_of_re_eq
equiv_limAux 📖	mathematical	—	CauSeq Real Real.instField Real.linearOrder Real.instIsStrictOrderedRing Complex instRing Norm.norm instNorm CauSeq.equiv isAbsoluteValueNorm CauSeq.const limAux	—	Real.instIsStrictOrderedRing IsAbsoluteValue.abs_isAbsoluteValue isCauSeq_re Real.instIsCompleteAbs Nat.instAtLeastTwoHAddOfNat isCauSeq_im isAbsoluteValueNorm lt_of_le_of_lt norm_le_abs_re_add_abs_im add_lt_add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT contravariant_lt_of_covariant_le covariant_swap_add_of_covariant_add add_halves CharZero.NeZero.two IsStrictOrderedRing.toCharZero exists_forall_ge_and CauSeq.equiv_lim half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono
im_le_norm 📖	mathematical	—	Real Real.instLE im Norm.norm Complex instNorm	—	abs_le Real.instIsOrderedAddMonoid abs_im_le_norm
instIsComplete 📖	mathematical	—	CauSeq.IsComplete Real Real.instField Real.linearOrder Real.instIsStrictOrderedRing Complex instRing Norm.norm instNorm isAbsoluteValueNorm	—	Real.instIsStrictOrderedRing isAbsoluteValueNorm equiv_limAux
isAbsoluteValueNorm 📖	mathematical	—	IsAbsoluteValue Real Real.semiring Real.partialOrder Complex instSemiring Norm.norm instNorm	—	norm_nonneg norm_eq_zero_iff norm_add_le norm_mul
isCauSeq_conj 📖	mathematical	—	IsCauSeq Real Real.instField Real.linearOrder Real.instIsStrictOrderedRing Complex instRing Norm.norm instNorm DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing	—	Real.instIsStrictOrderedRing DistribMulActionSemiHomClass.toAddMonoidHomClass instCharZero SemilinearMapClass.distribMulActionSemiHomClass RingHomClass.toLinearMapClassNNRat RingHom.instRingHomClass norm_conj
isCauSeq_im 📖	mathematical	—	IsCauSeq Real Real.instField Real.linearOrder Real.instIsStrictOrderedRing Real.instRing abs Real.lattice Real.instAddGroup im Complex instRing Norm.norm instNorm	—	Real.instIsStrictOrderedRing LE.le.trans_lt abs_im_le_norm CauSeq.cauchy
isCauSeq_norm 📖	mathematical	IsCauSeq Real Real.instField Real.linearOrder Real.instIsStrictOrderedRing Complex instRing Norm.norm instNorm	IsCauSeq Real Real.instField Real.linearOrder Real.instIsStrictOrderedRing Real.instRing abs Real.lattice Real.instAddGroup Complex Norm.norm instNorm	—	Real.instIsStrictOrderedRing lt_of_le_of_lt abs_norm_sub_norm_le
isCauSeq_re 📖	mathematical	—	IsCauSeq Real Real.instField Real.linearOrder Real.instIsStrictOrderedRing Real.instRing abs Real.lattice Real.instAddGroup re Complex instRing Norm.norm instNorm	—	Real.instIsStrictOrderedRing lt_of_le_of_lt abs_re_le_norm CauSeq.cauchy
lim_conj 📖	mathematical	—	CauSeq.lim Real Real.instField Real.linearOrder Real.instIsStrictOrderedRing Complex instRing Norm.norm instNorm isAbsoluteValueNorm instIsComplete cauSeqConj DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing	—	Real.instIsStrictOrderedRing ext isAbsoluteValueNorm instIsComplete IsAbsoluteValue.abs_isAbsoluteValue Real.instIsCompleteAbs isCauSeq_conj isCauSeq_re lim_re isCauSeq_im lim_im CauSeq.lim_neg
lim_eq_lim_im_add_lim_re 📖	mathematical	—	CauSeq.lim Real Real.instField Real.linearOrder Real.instIsStrictOrderedRing Complex instRing Norm.norm instNorm isAbsoluteValueNorm instIsComplete instAdd ofReal Real.instRing abs Real.lattice Real.instAddGroup IsAbsoluteValue.abs_isAbsoluteValue Real.instIsCompleteAbs cauSeqRe instMul cauSeqIm I	—	Real.instIsStrictOrderedRing CauSeq.lim_eq_of_equiv_const isAbsoluteValueNorm instIsComplete IsAbsoluteValue.abs_isAbsoluteValue Real.instIsCompleteAbs equiv_limAux CauSeq.ext ext isCauSeq_re MulZeroClass.mul_zero mul_one sub_self add_zero isCauSeq_im zero_add
lim_im 📖	mathematical	—	CauSeq.lim Real Real.instField Real.linearOrder Real.instIsStrictOrderedRing Real.instRing abs Real.lattice Real.instAddGroup IsAbsoluteValue.abs_isAbsoluteValue Real.instIsCompleteAbs cauSeqIm im Complex instRing Norm.norm instNorm isAbsoluteValueNorm instIsComplete	—	Real.instIsStrictOrderedRing IsAbsoluteValue.abs_isAbsoluteValue Real.instIsCompleteAbs isAbsoluteValueNorm instIsComplete lim_eq_lim_im_add_lim_re mul_one MulZeroClass.mul_zero add_zero zero_add
lim_norm 📖	mathematical	—	CauSeq.lim Real Real.instField Real.linearOrder Real.instIsStrictOrderedRing Real.instRing abs Real.lattice Real.instAddGroup IsAbsoluteValue.abs_isAbsoluteValue Real.instIsCompleteAbs cauSeqNorm Norm.norm Complex instNorm instRing isAbsoluteValueNorm instIsComplete	—	Real.instIsStrictOrderedRing CauSeq.lim_eq_of_equiv_const IsAbsoluteValue.abs_isAbsoluteValue Real.instIsCompleteAbs isAbsoluteValueNorm instIsComplete CauSeq.equiv_lim lt_of_le_of_lt abs_norm_sub_norm_le
lim_re 📖	mathematical	—	CauSeq.lim Real Real.instField Real.linearOrder Real.instIsStrictOrderedRing Real.instRing abs Real.lattice Real.instAddGroup IsAbsoluteValue.abs_isAbsoluteValue Real.instIsCompleteAbs cauSeqRe re Complex instRing Norm.norm instNorm isAbsoluteValueNorm instIsComplete	—	Real.instIsStrictOrderedRing IsAbsoluteValue.abs_isAbsoluteValue Real.instIsCompleteAbs isAbsoluteValueNorm instIsComplete lim_eq_lim_im_add_lim_re MulZeroClass.mul_zero mul_one sub_self add_zero
ne_zero_of_one_lt_re 📖	—	Real Real.instLT Real.instOne re	—	—	ne_zero_of_re_pos LT.lt.trans zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing
ne_zero_of_re_pos 📖	—	Real Real.instLT Real.instZero re	—	—	LT.lt.false zero_re
nndist_conj_self 📖	mathematical	—	NNDist.nndist Complex PseudoMetricSpace.toNNDist SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring NNReal.instSemiring instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.instAtLeastTwoHAddOfNat MonoidWithZeroHom Real NonAssocSemiring.toMulZeroOneClass Real.semiring MonoidWithZeroHom.funLike Real.nnabs im	—	NNReal.eq Nat.instAtLeastTwoHAddOfNat dist_nndist NNReal.coe_mul NNReal.coe_two Real.coe_nnabs dist_conj_self
nndist_of_im_eq 📖	mathematical	im	NNDist.nndist Complex PseudoMetricSpace.toNNDist SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup Real Real.pseudoMetricSpace re	—	NNReal.eq dist_of_im_eq
nndist_of_re_eq 📖	mathematical	re	NNDist.nndist Complex PseudoMetricSpace.toNNDist SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup Real Real.pseudoMetricSpace im	—	NNReal.eq dist_of_re_eq
nndist_self_conj 📖	mathematical	—	NNDist.nndist Complex PseudoMetricSpace.toNNDist SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring NNReal.instSemiring instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.instAtLeastTwoHAddOfNat MonoidWithZeroHom Real NonAssocSemiring.toMulZeroOneClass Real.semiring MonoidWithZeroHom.funLike Real.nnabs im	—	Nat.instAtLeastTwoHAddOfNat nndist_comm nndist_conj_self
nnnorm_I 📖	mathematical	—	NNNorm.nnnorm Complex SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup I NNReal NNReal.instOne	—	Real.instZeroLEOneClass norm_I norm_nonneg
nnnorm_natCast 📖	mathematical	—	NNNorm.nnnorm Complex SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup instNatCast NNReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring NNReal.instSemiring	—	norm_natCast NNReal.coe_natCast
nnnorm_nnratCast 📖	mathematical	—	NNNorm.nnnorm Complex SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup NNRat.cast instNNRatCast NNReal NNReal.instNNRatCast	—	Real.instIsStrictOrderedRing norm_nnratCast norm_nonneg
nnnorm_ofNat 📖	mathematical	—	NNNorm.nnnorm Complex SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup NNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring NNReal.instSemiring	—	nnnorm_natCast
nnnorm_ratCast 📖	mathematical	—	NNNorm.nnnorm Complex SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup instRatCast Real Real.normedAddCommGroup Real.instRatCast	—	nnnorm_real
nnnorm_real 📖	mathematical	—	NNNorm.nnnorm Complex SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup ofReal Real Real.normedAddCommGroup	—	NNReal.eq norm_real
normSq_eq_norm_sq 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom Complex Real NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instSemiring Real.semiring MonoidWithZeroHom.funLike normSq Monoid.toPow Real.instMonoid Norm.norm instNorm	—	sq Real.mul_self_sqrt normSq_nonneg
normSq_ofReal_add_I_mul_sqrt_one_sub 📖	mathematical	Real Real.instLE Norm.norm Real.norm Real.instOne	DFunLike.coe MonoidWithZeroHom Complex Real NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instSemiring Real.semiring MonoidWithZeroHom.funLike normSq instAdd ofReal instMul I Real.sqrt Real.instSub Real.instOne Monoid.toPow Real.instMonoid	—	mul_comm normSq_add_mul_I Real.sq_sqrt le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul 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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add 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 mul_nonneg_of_nonpos_of_nonpos AddGroup.existsAddOfLE IsOrderedRing.toMulPosMono covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le abs_le add_sub_cancel
normSq_ofReal_sub_I_mul_sqrt_one_sub 📖	mathematical	Real Real.instLE Norm.norm Real.norm Real.instOne	DFunLike.coe MonoidWithZeroHom Complex Real NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instSemiring Real.semiring MonoidWithZeroHom.funLike normSq instSub ofReal instMul I Real.sqrt Real.instSub Real.instOne Monoid.toPow Real.instMonoid	—	normSq_neg neg_sub' sub_neg_eq_add ofReal_neg Even.neg_pow Nat.instAtLeastTwoHAddOfNat normSq_ofReal_add_I_mul_sqrt_one_sub norm_neg
norm_I 📖	mathematical	—	Norm.norm Complex instNorm I Real Real.instOne	—	normSq_I Real.sqrt_one
norm_add_le' 📖	mathematical	—	Real Real.instLE Norm.norm Complex instNorm instAdd Real.instAdd	—	mul_self_le_mul_self_iff IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg add_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid norm_mul_self_eq_normSq Nat.instAtLeastTwoHAddOfNat add_mul_self_eq add_right_comm normSq_add mul_assoc norm_def Real.sqrt_mul normSq_nonneg normSq_conj map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass add_le_add_right mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono re_le_norm le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo
norm_add_mul_I 📖	mathematical	—	Norm.norm Complex instNorm instAdd ofReal instMul I Real.sqrt Real Real.instAdd Monoid.toPow Real.instMonoid	—	normSq_add_mul_I
norm_conj 📖	mathematical	—	Norm.norm Complex instNorm DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing	—	normSq_conj
norm_def 📖	mathematical	—	Norm.norm Complex instNorm Real.sqrt DFunLike.coe MonoidWithZeroHom Real NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instSemiring Real.semiring MonoidWithZeroHom.funLike normSq	—	—
norm_div 📖	mathematical	—	Norm.norm Complex instNorm DivInvMonoid.toDiv instDivInvMonoid Real Real.instDivInvMonoid	—	norm_def normSq_div Real.sqrt_div normSq_nonneg
norm_eq_sqrt_sq_add_sq 📖	mathematical	—	Norm.norm Complex instNorm Real.sqrt Real Real.instAdd Monoid.toPow Real.instMonoid re im	—	norm_def normSq_apply sq
norm_eq_zero_iff 📖	mathematical	—	Norm.norm Complex instNorm Real Real.instZero instZero	—	Real.sqrt_eq_zero normSq_nonneg normSq_eq_zero
norm_intCast 📖	mathematical	—	Norm.norm Complex instNorm instIntCast abs Real Real.lattice Real.instAddGroup Real.instIntCast	—	ofReal_intCast norm_real Real.norm_eq_abs
norm_int_of_nonneg 📖	mathematical	—	Norm.norm Complex instNorm instIntCast Real Real.instIntCast	—	norm_intCast Int.cast_abs Real.instIsStrictOrderedRing abs_of_nonneg Int.instAddLeftMono
norm_le_abs_re_add_abs_im 📖	mathematical	—	Real Real.instLE Norm.norm Complex instNorm Real.instAdd abs Real.lattice Real.instAddGroup re im	—	re_add_im norm_real norm_mul norm_I mul_one norm_add_le
norm_le_sqrt_two_mul_max 📖	mathematical	—	Real Real.instLE Norm.norm Complex instNorm Real.instMul Real.sqrt instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instMax abs Real.lattice Real.instAddGroup re im	—	Nat.instAtLeastTwoHAddOfNat le_max_of_le_left abs_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Real.sqrt_monotone add_le_add sq_le_sq Real.instIsStrictOrderedRing abs_of_nonneg le_max_left le_max_right two_mul Real.sqrt_mul le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Real.sqrt_sq
norm_map_zero' 📖	mathematical	—	Norm.norm Complex instNorm instZero Real Real.instZero	—	norm_eq_zero_iff
norm_mul 📖	mathematical	—	Norm.norm Complex instNorm instMul Real Real.instMul	—	norm_def normSq_mul Real.sqrt_mul normSq_nonneg
norm_mul_self_eq_normSq 📖	mathematical	—	Real Real.instMul Norm.norm Complex instNorm DFunLike.coe MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instSemiring Real.semiring MonoidWithZeroHom.funLike normSq	—	Real.mul_self_sqrt normSq_nonneg
norm_natCast 📖	mathematical	—	Norm.norm Complex instNorm instNatCast Real Real.instNatCast	—	norm_of_nonneg Nat.cast_nonneg Real.instIsOrderedRing
norm_neg' 📖	mathematical	—	Norm.norm Complex instNorm instNeg	—	norm_def normSq_neg
norm_nnratCast 📖	mathematical	—	Norm.norm Complex instNorm NNRat.cast instNNRatCast Real Real.instNNRatCast	—	norm_of_nonneg NNRat.cast_nonneg Real.instIsStrictOrderedRing
norm_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero Norm.norm Complex instNorm	—	Real.sqrt_nonneg
norm_ofNat 📖	mathematical	—	Norm.norm Complex instNorm Real instOfNatAtLeastTwo Real.instNatCast	—	norm_natCast
norm_of_nonneg 📖	mathematical	Real Real.instLE Real.instZero	Norm.norm Complex instNorm ofReal	—	norm_real abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
norm_pow 📖	mathematical	—	Norm.norm Complex instNorm Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring Real Real.instMonoid	—	map_pow MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass isAbsoluteValueNorm Real.instIsDomain instNontrivial
norm_prod 📖	mathematical	—	Norm.norm Complex instNorm Finset.prod CommRing.toCommMonoid commRing Real Real.instCommMonoid	—	map_prod MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass isAbsoluteValueNorm Real.instIsDomain instNontrivial
norm_ratCast 📖	mathematical	—	Norm.norm Complex instNorm instRatCast abs Real Real.lattice Real.instAddGroup Real.instRatCast	—	norm_real
norm_real 📖	mathematical	—	Norm.norm Complex instNorm ofReal Real Real.norm	—	normSq_ofReal Real.sqrt_mul_self_eq_abs
norm_sub_one_sq_eqOn_sphere 📖	mathematical	—	Set.EqOn Complex Real Monoid.toPow Real.instMonoid Norm.norm instNorm instSub instOne Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instSub Real.instOne re Metric.sphere SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup instZero	—	norm_sub_one_sq_eq_of_norm_eq_one sub_zero
norm_sub_one_sq_eq_of_norm_eq_one 📖	mathematical	Norm.norm Complex instNorm Real Real.instOne	Real Monoid.toPow Real.instMonoid Norm.norm Complex instNorm instSub instOne Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instSub Real.instOne re	—	sq_eq_one_iff IsStrictOrderedRing.noZeroDivisors Real.instIsStrictOrderedRing AddGroup.existsAddOfLE Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.sub_pf 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.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt 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_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.lt_of_eq_of_lt neg_eq_zero sub_eq_zero_of_eq normSq_apply sq_norm Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Nat.instAtLeastTwoHAddOfNat sub_zero Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.instAtLeastTwo
norm_sub_one_sq_eq_of_norm_one 📖	mathematical	Norm.norm Complex instNorm Real Real.instOne	Real Monoid.toPow Real.instMonoid Norm.norm Complex instNorm instSub instOne Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instSub Real.instOne re	—	norm_sub_one_sq_eq_of_norm_eq_one
norm_two 📖	mathematical	—	Norm.norm Complex instNorm instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat Real Real.instNatCast	—	norm_ofNat Nat.instAtLeastTwoHAddOfNat
norm_zpow 📖	mathematical	—	Norm.norm Complex instNorm DivInvMonoid.toZPow instDivInvMonoid Real Real.instDivInvMonoid	—	map_zpow₀ MonoidWithZeroHom.monoidWithZeroHomClass isAbsoluteValueNorm Real.instIsDomain instNontrivial
one_le_normSq_iff 📖	mathematical	—	Real Real.instLE Real.instOne DFunLike.coe MonoidWithZeroHom Complex NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instSemiring Real.semiring MonoidWithZeroHom.funLike normSq Norm.norm instNorm	—	one_le_sq_iff₀ IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass norm_nonneg normSq_eq_norm_sq
one_lt_normSq_iff 📖	mathematical	—	Real Real.instLT Real.instOne DFunLike.coe MonoidWithZeroHom Complex NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instSemiring Real.semiring MonoidWithZeroHom.funLike normSq Norm.norm instNorm	—	one_lt_sq_iff₀ IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass norm_nonneg normSq_eq_norm_sq
range_norm 📖	mathematical	—	Set.range Real Complex Norm.norm instNorm Set.Ici Real.instPreorder Real.instZero	—	Set.Subset.antisymm Set.range_subset_iff norm_nonneg norm_of_nonneg
range_normSq 📖	mathematical	—	Set.range Real Complex DFunLike.coe MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instSemiring Real.semiring MonoidWithZeroHom.funLike normSq Set.Ici Real.instPreorder Real.instZero	—	Set.Subset.antisymm Set.range_subset_iff normSq_nonneg normSq_ofReal Real.mul_self_sqrt
re_le_norm 📖	mathematical	—	Real Real.instLE re Norm.norm Complex instNorm	—	abs_le Real.instIsOrderedAddMonoid abs_re_le_norm
re_neg_ne_zero_of_one_lt_re 📖	—	Real Real.instLT Real.instOne re	—	—	re_neg_ne_zero_of_re_pos LT.lt.trans zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing
re_neg_ne_zero_of_re_pos 📖	—	Real Real.instLT Real.instZero re	—	—	ne_iff_lt_or_gt neg_lt_zero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid neg_re
sq_norm 📖	mathematical	—	Real Monoid.toPow Real.instMonoid Norm.norm Complex instNorm DFunLike.coe MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instSemiring Real.semiring MonoidWithZeroHom.funLike normSq	—	normSq_eq_norm_sq
sq_norm_sub_sq_im 📖	mathematical	—	Real Real.instSub Monoid.toPow Real.instMonoid Norm.norm Complex instNorm im re	—	sq_norm_sub_sq_re sub_sub_cancel
sq_norm_sub_sq_re 📖	mathematical	—	Real Real.instSub Monoid.toPow Real.instMonoid Norm.norm Complex instNorm re im	—	sq_norm normSq_apply sq add_sub_cancel_left

---

← Back to Index