pi π | CompOp | 1068 mathmath: cos_add_nat_mul_pi, Angle.abs_toReal_neg_coe_eq_self_iff, pi_div_four_le_arcsin, Polynomial.Chebyshev.isExtrOn_T_real_iff, Complex.cos_sub_pi, hasDerivAt_fourier, Complex.log_conj_eq_ite, EuclideanGeometry.angle_le_pi_div_two_of_angle_eq_pi_div_two, Circle.periodic_exp, Sbtw.oangleβββ_eq_pi, Orientation.oangle_eq_zero_or_eq_pi_iff_right_eq_smul, tan_pi_div_four, cos_pi_div_five, Polynomial.mahlerMeasure_def_of_ne_zero, EulerSine.integral_cos_mul_cos_pow, Complex.tendsto_log_nhdsWithin_im_neg_of_re_neg_of_im_zero, Complex.log_I, Complex.norm_circleTransformBoundingFunction_le, Angle.sign_two_zsmul_eq_sign_iff, Complex.log_neg_one, norm_torusIntegral_le_of_norm_le_const, EuclideanGeometry.Sphere.thales_theorem, completedZeta_eq_tsum_of_one_lt_re, mellin_eq_fourier, Affine.Triangle.oangle_excenter_singleton_eq_add_pi, EuclideanGeometry.abs_oangle_right_toReal_lt_pi_div_two_of_dist_eq, pi_le_four, MeasureTheory.charFun_eq_fourierIntegral', hasFDerivAt_fourierChar_neg_bilinear_left, tan_pi_sub, arcsin_eq_pi_div_two_sub_arccos, EisensteinSeries.hasSum_e2Summand_symmetricIcc, InnerProductSpace.volume_closedBall_of_dim_even, Complex.Gammaβ_def, Orientation.inner_rotation_pi_div_two_right_smul, Orientation.oangle_add_left_smul_rotation_pi_div_two, Complex.sin_pi_div_two_sub, HurwitzZeta.hasSum_int_cosKernelβ, cos_add_pi, Complex.exp_eq_exp_iff_exists_int, InnerProductGeometry.angle_add_angle_sub_add_angle_sub_eq_pi, sin_pi_div_two, EuclideanGeometry.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero, HurwitzZeta.LSeriesHasSum_cos, fourierIntegralInv_eq', Angle.two_zsmul_eq_pi_iff, InnerProductGeometry.angle_neg_self_of_nonzero, sin_add_two_pi, Angle.sin_add_pi_div_two, Stirling.factorial_isEquivalent_stirling, Complex.tan_nat_mul_pi_sub, norm_jacobiThetaβ_term_le, cos_sub_pi, Complex.norm_sub_mem_Icc_angle, cos_eq_zero_iff, rpow_eq_nhds_of_neg, norm_jacobiThetaβ_term_fderiv_ge, tan_int_mul_pi, summableLocallyUniformlyOn_iteratedDerivWithin_cexp, AddCircle.homeomorphCircle'_apply_mk, neg_pi_div_two_eq_arcsin, Polynomial.Chebyshev.integral_measureT_eq_integral_cos, Orientation.tan_oangle_add_left_smul_rotation_pi_div_two, Complex.cos_eq_one_iff, mapsTo_cos_Ioo, sin_periodic, ModularForm.eta_q_eq_pow, EuclideanGeometry.angle_le_pi, circleIntegral_def_Icc, ZMod.LFunction_one_sub, Complex.arg_neg_I, Gamma_nat_add_half, EuclideanGeometry.oangle_eq_pi_sub_two_zsmul_oangle_of_dist_eq, circleIntegrable_iff, Complex.tsum_exp_neg_mul_int_sq, fderiv_fourierChar_neg_bilinear_right_apply, one_add_mul_le_cos, cos_int_mul_two_pi, SchwartzMap.lineDerivOp_fourier_eq, NumberField.dedekindZeta_residue_def, Angle.sin_eq_zero_iff, Complex.tan_pi_sub, circleMap_neg_pi_div_two, Orientation.neg_rotation, GaussianFourier.integral_cexp_neg_mul_sq_norm, Sbtw.oangle_eq_add_pi_left, Function.Periodic.norm_qParam_le_of_one_half_le_im, Complex.angle_exp_one, circleIntegral.integral_sub_inv_of_mem_ball, hasSum_one_div_nat_pow_mul_fourier, Complex.cos_eq_zero_iff, GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace, Complex.cos_antiperiodic, Complex.cos_add_nat_mul_two_pi, TemperedDistribution.lineDerivOp_fourier_eq, HasProdUniformlyOn_sineTerm_prod_on_compact, HurwitzZeta.cosZeta_two_mul_nat, tendsto_cos_pi_div_two, Complex.norm_eq_one_iff', Complex.sin_eq_neg_one_iff, riemannZeta_two, isIntegral_two_mul_sin_rat_mul_pi, Orientation.tan_oangle_add_right_smul_rotation_pi_div_two, Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable_aux, fourierIntegral_gaussian_innerProductSpace', fourier_gaussian_pi', integral_log_sin_zero_pi_div_two, iteratedDerivWithin_tsum_cexp_eq, jacobiThetaβ_functional_equation, sin_two_pi, EuclideanGeometry.dist_eq_add_dist_iff_angle_eq_pi, EuclideanGeometry.pi_div_three_le_angle_of_le_of_le, Complex.sin_int_mul_pi, GaussianFourier.integral_cexp_neg_mul_sq_norm_add, Complex.sin_eq_zero_iff, NumberField.abs_discr_ge', sum_cauchyPowerSeries_eq_integral, Complex.tan_pi_div_two_sub, Angle.toReal_coe_eq_self_iff_mem_Ioc, vector_fourierIntegral_eq_integral_exp_smul, HurwitzZeta.evenKernel_def, range_arctan, fourier_real_eq_integral_exp_smul, pi_nonneg, NumberField.abs_discr_ge, Complex.arg_le_pi, AddCircle.homeomorphCircle'_symm_apply, Polynomial.Chebyshev.eval_T_real_eq_neg_one_iff, Orientation.oangle_eq_pi_iff_oangle_rev_eq_pi, Orientation.oangle_neg_right, HurwitzZeta.jacobiThetaβ'_functional_equation', Function.Periodic.norm_qParam_lt_iff, Wallis.W_le, Complex.cos_pi_div_two, sin_pi_sub, Circle.isAddQuotientCoveringMap_exp, sin_pi, hasSum_nat_jacobiTheta, fourier_deriv, Polynomial.Chebyshev.integral_T_real_mul_self_measureT_of_ne_zero, ZMod.stdAddChar_coe, DifferentiableOn.circleIntegral_sub_inv_smul, Angle.abs_toReal_eq_pi_div_two_iff, Angle.toReal_eq_pi_iff, Complex.neg_pi_div_two_lt_arg_iff, cos_add_int_mul_two_pi, integral_sin_pow_pos, Angle.abs_toReal_le_pi, Complex.integral_rpow_mul_exp_neg_rpow, sin_pi_div_three, Complex.arg_mul_eq_add_arg_iff, Complex.sin_nat_mul_pi, Circle.exp_eq_exp, Complex.tan_int_mul_pi, Complex.volume_sum_rpow_le, EuclideanGeometry.dist_eq_iff_eq_smul_rotation_pi_div_two_vadd_midpoint, ModularForm.tsum_logDeriv_eta_q, Complex.mul_angle_le_norm_sub, Polynomial.Chebyshev.isLocalMin_T_real, Complex.integral_circleTransform, Polynomial.toAddCircle_X_pow_eq_fourier, Complex.arg_le_pi_div_two_iff, Angle.toReal_coe, HurwitzZeta.oddKernel_def', Circle.exp_two_pi_mul_int, arctan_mem_Ioo, fourier_gaussian_innerProductSpace, Complex.tan_nat_mul_pi, AddCircle.scaled_exp_map_periodic, InnerProductGeometry.norm_sub_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two, Complex.isPrimitiveRoot_exp_rat, Orientation.neg_rotation_neg_pi_div_two, Polynomial.Chebyshev.integral_measureT_eq_integral_cos_of_continuous, VectorFourier.fourierPowSMulRight_eq_comp, Complex.mem_rootsOfUnity, sin_add_int_mul_pi, Polynomial.isRoot_cos_pi_div_five, Complex.sin_int_mul_two_pi_sub, image_circleMap_Ioc, neg_pi_div_two_lt_arctan, cos_nat_mul_two_pi_sub_pi, Complex.cos_nat_mul_two_pi_sub_pi, sin_antiperiodic, sin_sub_pi_div_two, Complex.circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable, tan_int_mul_pi_div_two, Wallis.tendsto_W_nhds_pi_div_two, Angle.sign_two_nsmul_eq_neg_sign_iff, cos_add_two_pi, isIntegral_two_mul_cos_rat_mul_pi, HurwitzZeta.hasSum_nat_sinZeta, Angle.toReal_pi, EuclideanGeometry.angle_orthogonalProjection_self, EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_neg_pi_div_two, Complex.exp_antiperiodic, fourierCoeff_bernoulli_eq, Complex.exp_add_pi_mul_I, Complex.log_exp_eq_re_add_toIocMod, circleMap_eq_circleMap_iff, Gamma_mul_Gamma_add_half, Complex.log_inv_eq_ite, Orientation.oangle_eq_pi_iff_angle_eq_pi, two_mul_arctan_inv_2_sub_arctan_inv_7, EulerSine.integral_cos_mul_cos_pow_aux, SchwartzMap.fourier_lineDerivOp_eq, Angle.toReal_mem_Ioc, antitoneOn_cos, Angle.toReal_neg_pi_div_two, pi_lt_d6, Angle.sign_pi_sub, sin_add_nat_mul_pi, cos_nat_mul_pi, InnerProductGeometry.angle_le_pi, InnerProductGeometry.norm_add_eq_norm_sub_iff_angle_eq_pi_div_two, TemperedDistribution.fourierInv_lineDerivOp_eq, pi_div_two_le_two, Stirling.le_log_factorial_stirling, EuclideanGeometry.Sphere.IsTangentAt.angle_eq_pi_div_two, Complex.arg_of_re_neg_of_im_nonneg, riemannZeta_one_sub, arcsin_eq_pi_div_two, EuclideanSpace.volume_closedBall_fin_three, hasSum_zeta_four, cos_pi_div_four, Complex.tan_eq_zero_iff', Complex.cos_nat_mul_two_pi, TemperedDistribution.laplacian_eq_fourierMultiplierCLM, Angle.sign_eq_zero_iff, Orientation.rotation_pi_apply, cauchyPowerSeries_apply, Angle.two_nsmul_toReal_eq_two_mul_sub_two_pi, tan_nat_mul_pi_sub, EuclideanGeometry.Sphere.oangle_eq_pi_sub_two_zsmul_oangle_center_left, arccos_eq_pi_div_two_sub_arcsin, Angle.sin_add_pi, Angle.toReal_coe_eq_self_iff, Gamma_mul_Gamma_one_sub, Complex.sin_sub_nat_mul_two_pi, DiffContOnCl.circleIntegral_sub_inv_smul, Complex.arg_neg_eq_arg_sub_pi_of_im_pos, Complex.ofReal_cpow_of_nonpos, arcsin_le_pi_div_two, Complex.sin_nat_mul_two_pi_sub, cos_two_pi, EuclideanGeometry.oangle_pointReflection_left, mul_le_sin, InnerProductGeometry.angle_neg_right, tsum_exp_neg_mul_int_sq, HurwitzZeta.expZeta_one_sub, EuclideanGeometry.oangle_eq_pi_iff_sbtw, arccos_image_Icc, InnerProductGeometry.angle_zero_right, cos_pi_div_sixteen, fourierIntegral_gaussian_pi, Angle.cos_add_pi, iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow, Angle.two_zsmul_coe_pi, circleAverage_eq_circleIntegral, Angle.cos_add_pi_div_two, cos_two_pi_sub, arctan_add_arctan_lt_pi_div_two, Angle.two_nsmul_eq_zero_iff, Complex.arg_mul_cos_add_sin_mul_I_eq_toIocMod, VectorFourier.norm_iteratedFDeriv_fourierPowSMulRight, InnerProductGeometry.sin_eq_one_iff_angle_eq_pi_div_two, Complex.arg_cos_add_sin_mul_I_sub, Angle.cos_nonneg_iff_abs_toReal_le_pi_div_two, mellinInv_eq_fourierIntegralInv, Gamma_one_half_eq, cot_series_rep', pi_div_two_eq_arcsin, two_le_pi, Complex.cos_pi_sub, Complex.integral_exp_neg_rpow, polarCoord_target, Orientation.oangle_neg_self_left, pi_div_two_pos, Complex.hasDerivAt_Gammaβ_one, arctan_eq_neg_pi_div_four, InnerProductGeometry.angle_add_le_pi_div_two_of_inner_eq_zero, Sbtw.oangle_eq_add_pi_right, circleMap_pi_div_two, riemannZeta_four, Angle.neg_pi_lt_toReal, HurwitzZeta.hasSum_nat_completedCosZeta, Polynomial.toAddCircle.integrable, Complex.cos_sub_two_pi, Complex.sin_sub_two_pi, cos_le_one_sub_mul_cos_sq, Complex.sin_sub_pi_div_two, norm_cauchyPowerSeries_le, mellinInv_eq_fourierInv, Complex.abs_arg_le_pi, EuclideanGeometry.Sphere.tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center, arccos_le_pi, fourier_gaussian_innerProductSpace', HurwitzZeta.hasSum_int_cosKernel, Angle.coe_eq_zero_iff, tendsto_integral_gaussian_smul', EuclideanGeometry.angle_le_pi_div_three_of_le_of_le, Polynomial.Chebyshev.isLocalMax_T_real, tendsto_cos_neg_pi_div_two, norm_jacobiThetaβ_term, Complex.exp_neg_pi_div_two_mul_I, ZetaAsymptotics.tendsto_Gamma_term_aux, tan_pi_div_two, Circle.exp_two_pi, arccos_le_pi_div_two, EisensteinSeries.D2_S, Polynomial.int_cyclotomic_rw, Complex.tan_int_mul_pi_div_two, EisensteinSeries.G2_S_transform, Complex.isIntegral_exp_rat_mul_pi_mul_I, DiffContOnCl.deriv_eq_smul_circleIntegral, EuclideanSpace.volume_closedBall_fin_two, DifferentiableOn.deriv_eq_smul_circleIntegral, sq_cos_pi_div_six, Angle.two_zsmul_toReal_eq_two_mul_sub_two_pi, abs_cos_int_mul_pi, Complex.cos_int_mul_two_pi_sub, Complex.tendsto_arg_nhdsWithin_im_nonneg_of_re_neg_of_im_zero, tendsto_sin_neg_pi_div_two, Angle.cos_sub_pi, Stirling.le_factorial_stirling, EuclideanGeometry.angle_self_right, tendsto_logDeriv_euler_sin_div, fourierIntegral_iteratedDeriv, logDeriv_sin_div_eq_cot, HurwitzZeta.cosZeta_one_sub, EulerSine.sin_pi_mul_eq, Complex.arg_neg_eq_arg_add_pi_iff, HurwitzZeta.hasSum_nat_sinKernel, Complex.inv_cpow_eq_ite', Complex.isPrimitiveRoot_iff, arcsin_neg_one, EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_pi_div_two, Complex.exp_periodic, sin_nat_mul_two_pi_sub, norm_exp_mul_sq_le, Complex.exp_nat_mul_two_pi_mul_I, Complex.log_exp_eq_sub_toIocDiv, HurwitzKernelBounds.F_nat_one_le, isAlgebraic_tan_rat_mul_pi, Affine.Triangle.acuteAngled_iff_angle_lt, Polynomial.intervalIntegrable_mahlerMeasure, sin_pi_div_two_sub, SchwartzMap.lineDeriv_eq_fourierMultiplierCLM, Complex.isAlgebraic_sin_rat_mul_pi, arccos_eq_pi_div_two, Complex.isPrimitiveRoot_exp_of_isCoprime, circleIntegral.norm_integral_le_of_norm_le_const, arcsin_mem_Icc, InnerProductGeometry.sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi, Sbtw.oangleβββ_eq_pi, DiffContOnCl.circleIntegral_one_div_sub_center_pow_smul, arccos_neg, isAlgebraic_cos_rat_mul_pi, cos_pi_div_two, Angle.tan_sub_pi, Angle.sub_coe_pi_eq_add_coe_pi, rpow_def_of_neg, Angle.sign_coe_pi, Orientation.inner_rotation_pi_div_two_right, EuclideanGeometry.sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi, Complex.arg_one_add_mem_Ioo, Function.Periodic.im_invQParam, Angle.sin_eq_iff_coe_eq_or_add_eq_pi, Complex.sin_two_pi, UpperHalfPlane.norm_exp_two_pi_I_lt_one, ProbabilityTheory.cauchyPDFReal_def, HurwitzZeta.hasSum_int_cosZeta, Angle.toReal_mem_Ioo_iff_sign_pos, Complex.arg_exp_mul_I, Complex.arg_of_re_neg_of_im_neg, EuclideanGeometry.oangle_eq_pi_iff_angle_eq_pi, pi_upper_bound_start, tan_sub_pi, pow_mul_norm_iteratedFDeriv_fourier_le, Angle.toReal_pi_div_two, pi_pos, Complex.cos_add_pi, ZetaAsymptotics.tendsto_riemannZeta_sub_one_div_Gammaβ, Complex.tendsto_norm_tan_atTop, arctan_inv_of_neg, Angle.sign_sub_pi, Orientation.inner_rotation_pi_div_two_left, Complex.hasDerivAt_Gammaβ_one, Complex.sin_add_two_pi, EisensteinSeries.hasSum_e2Summand_symmetricIco, ModularForm.eta_q_eq_cexp, Affine.Triangle.circumsphere_eq_of_dist_of_oangle, arccos_le_pi_div_four, cos_int_mul_pi_sub, Complex.arg_lt_pi_div_two_iff, Complex.arg_mem_Ioc, InnerProductSpace.volume_ball, circleIntegral.norm_two_pi_i_inv_smul_integral_le_of_norm_le_const, EuclideanGeometry.two_zsmul_oangle_self_orthogonalProjection, Complex.tendsto_arg_nhdsWithin_im_neg_of_re_neg_of_im_zero, EisensteinSeries.q_expansion_riemannZeta, fourierIntegral_real_eq_integral_exp_smul, fourier_coe_apply, cos_pi_div_eight, deriv_fourierIntegral, norm_jacobiTheta_sub_one_le, HurwitzZeta.hasSum_nat_cosZeta, injOn_tan, Angle.toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff, hasSum_cauchyPowerSeries_integral, Complex.tan_sub_int_mul_pi, Complex.sin_eq_sin_iff, Circle.exp_inj, Angle.two_zsmul_neg_pi_div_two, Orientation.inner_rotation_pi_div_two_left_smul, EuclideanGeometry.Sphere.abs_oangle_center_left_toReal_lt_pi_div_two, InnerProductGeometry.inner_eq_neg_mul_norm_iff_angle_eq_pi, InnerProductGeometry.cos_eq_zero_iff_angle_eq_pi_div_two, InnerProductGeometry.angle_sub_le_pi_div_two_of_inner_eq_zero, HasProdLocallyUniformlyOn_euler_sin_prod, Circle.exp_add_two_pi, Complex.sin_pi_sub, Wallis.W_eq_integral_sin_pow_div_integral_sin_pow, EuclideanGeometry.angle_eq_angle_add_pi_div_two_of_oangle_eq_add_pi_of_sSameSide, has_antideriv_at_fourier_neg, Angle.two_zsmul_toReal_eq_two_mul, HurwitzZeta.hasSum_expZeta_of_one_lt_re, Complex.neg_pi_lt_arg, HurwitzZeta.hasSum_int_evenKernel, sin_nat_mul_pi, Complex.inv_cpow_eq_ite, hasSum_one_div_nat_pow_mul_cos, hasStrictDerivAt_const_rpow_of_neg, EuclideanGeometry.oangle_orthogonalProjection_self, ModularFormClass.exp_decay_sub_atImInfty, Circle.invOn_arg_exp, two_pi_pos, ProbabilityTheory.gaussianPDFReal_def, cos_eq_cos_iff, UpperHalfPlane.IsZeroAtImInfty.exp_decay_atImInfty, Complex.two_pi_I_inv_smul_circleIntegral_sub_sq_inv_smul_of_differentiable, Complex.arg_neg_eq_arg_add_pi_of_im_neg, InnerProductGeometry.angle_zero_left, Complex.arg_conj, InnerProductGeometry.angle_add_angle_eq_pi_of_angle_eq_pi, Complex.cos_sub_nat_mul_two_pi, EuclideanGeometry.sin_eq_one_iff_angle_eq_pi_div_two, sin_two_pi_sub, Complex.cos_int_mul_two_pi_add_pi, sinOrderIso_apply, hasDerivAt_fourier_neg, Angle.cos_eq_zero_iff, Angle.angle_eq_iff_two_pi_dvd_sub, InnerProductGeometry.cos_eq_neg_one_iff_angle_eq_pi, InnerProductSpace.volume_ball_of_dim_odd, Complex.arg_lt_pi_iff, SchwartzMap.fourierInv_lineDerivOp_eq, cos_int_mul_two_pi_add_pi, Complex.tendsto_euler_sin_prod, sin_eq_sin_iff, Complex.arg_eq_pi_div_two_iff, EulerSine.integral_sin_mul_sin_mul_cos_pow_eq, circleIntegral.norm_integral_lt_of_norm_le_const_of_lt, isBigO_at_im_infty_jacobiTheta_sub_one, Orientation.oangle_neg_left, Complex.tsum_exp_neg_quadratic, Angle.sin_coe_pi, circleAverage_def, Stirling.sqrt_pi_le_stirlingSeq, NumberField.Ideal.tendsto_norm_le_div_atTopβ, Complex.range_arg, Complex.isAddQuotientCoveringMap_exp, Complex.log_mul_eq_add_log_iff, Complex.cot_pi_eq_exp_ratio, pi_gt_d2, EuclideanGeometry.oangle_pointReflection_right, Complex.integral_exp_neg_mul_rpow, Complex.isIntegral_two_mul_sin_rat_mul_pi, EuclideanGeometry.oangle_add_oangle_add_oangle_eq_pi, EuclideanGeometry.Sphere.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center, EuclideanGeometry.oangle_eq_zero_or_eq_pi_iff_collinear, HurwitzZeta.hurwitzZetaEven_one_sub, EuclideanGeometry.Sphere.abs_oangle_center_right_toReal_lt_pi_div_two, Polynomial.Chebyshev.integral_eval_T_real_measureT_zero, hasSum_mellin_pi_mul, HurwitzZeta.hasSum_int_sinKernel, tan_pi_div_two_sub, arcsin_of_le_neg_one, cos_pi_sub, sin_int_mul_two_pi_sub, cot_series_rep, Complex.conj_cpow_eq_ite, Affine.Triangle.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_circumcenter, cos_pi_div_six, range_arcsin, Complex.sin_antiperiodic, EuclideanGeometry.angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two, HurwitzZeta.LSeriesHasSum_exp, InnerProductGeometry.angle_add_lt_pi_div_two_of_inner_eq_zero, Complex.neg_pi_lt_log_im, arccos_eq_pi, InnerProductGeometry.norm_sub_eq_add_norm_iff_angle_eq_pi, bernoulliFourierCoeff_eq, circleAverage_eq_integral_add, Gamma_nat_add_one_add_half, Complex.isPrimitiveRoot_exp_of_coprime, Complex.tan_sub_nat_mul_pi, pi_lt_four, Polynomial.Chebyshev.rootMultiplicity_T_real, tan_periodic, periodic_circleMap, ModularForm.logDeriv_eta_eq_E2, TemperedDistribution.fourier_lineDerivOp_eq, Complex.sin_eq_one_iff, Angle.sign_two_nsmul_eq_sign_iff, Complex.volume_sum_rpow_lt, iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow, fourier_iteratedDeriv, Complex.cos_periodic, integral_univ_inv_one_add_sq, sin_int_mul_pi_sub, arcsin_le_neg_pi_div_two, Complex.exp_pi_div_two_mul_I, Orientation.oangle_sub_right_smul_rotation_pi_div_two, Angle.sin_pi_div_two_sub, sin_add_pi_div_two, VectorFourier.fourierSMulRight_apply, Sbtw.angleβββ_eq_pi, integral_cexp_quadratic, cos_sub_nat_mul_two_pi, Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable, Complex.tan_sub_pi, Unitary.openPartialHomeomorph_target, Complex.Gammaβ_def, Complex.tan_add_pi, one_le_pi_div_two, pi_gt_sqrtTwoAddSeries, Complex.isPrimitiveRoot_exp_rat_of_even_num, EuclideanGeometry.cos_eq_neg_one_iff_angle_eq_pi, Complex.abs_arg_le_pi_div_two_iff, VectorFourier.pow_mul_norm_iteratedFDeriv_fourierIntegral_le, Angle.two_zsmul_eq_iff, hasDerivAt_fourier, Complex.isPrimitiveRoot_exp, one_sub_mul_le_cos, Polynomial.Chebyshev.isMinOn_T_real, circleMap_neg_radius, Angle.two_nsmul_toReal_eq_two_mul_add_two_pi, Angle.sign_pi_add, Complex.isIntegral_exp_neg_rat_mul_pi_mul_I, tan_nat_mul_pi, mellin_eq_fourierIntegral, InnerProductGeometry.angle_eq_angle_add_angle_iff, HurwitzZeta.hasSum_nat_completedSinZeta, Orientation.oangle_neg_self_right, fourierIntegral_eq', NNReal.coe_real_pi, Polynomial.Chebyshev.isLocalExtr_T_real_iff, hasFPowerSeriesOn_cauchy_integral, arctan_inv_2_add_arctan_inv_3, arctan_one, Complex.circleIntegral_div_sub_of_differentiable_on_off_countable, contDiffOn_tsum_cexp, Complex.Gammaβ_add_one, Complex.cos_add_pi_div_two, pi_lower_bound_start, Circle.argEquiv_symm_apply, AddCircle.toCircle_apply_mk, irrational_pi, Angle.two_nsmul_eq_pi_iff, Orientation.inner_smul_rotation_pi_div_two_right, fourierIntegral_gaussian_innerProductSpace, sin_pi_over_two_pow_succ, bijOn_sin, bijOn_cos, EisensteinSeries.qExpansion_identity_pnat, tan_add_int_mul_pi, iteratedDeriv_fourier, tan_pi_div_six, mul_abs_le_abs_sin, arccos_lt_pi, Orientation.oangle_eq_zero_or_eq_pi_iff_not_linearIndependent, InnerProductGeometry.angle_self_neg_of_nonzero, EuclideanGeometry.angle_eq_pi_sub_angle_div_two_of_oangle_eq_add_pi_of_sOppSide, Complex.angle_le_mul_norm_sub, Angle.sign_two_zsmul_eq_neg_sign_iff, EuclideanSpace.volume_ball_fin_three, arctan_inv_sqrt_three, cot_pi_mul_contDiffWithinAt, cos_sub_int_mul_pi, integral_log_sin_zero_pi, InnerProductGeometry.angle_sub_lt_pi_div_two_of_inner_eq_zero, arcsin_of_one_le, pi_lt_d2, jacobiThetaβ'_add_left', Polynomial.toAddCircle_monomial_eq_smul_fourier, jacobiThetaβ'_functional_equation, Angle.abs_toReal_add_abs_toReal_eq_pi_of_two_zsmul_add_eq_zero_of_sign_eq, sin_sub_int_mul_pi, riemannZeta_one, EuclideanGeometry.angle_lt_pi_div_two_of_angle_eq_pi_div_two, tendsto_tan_pi_div_two, ProbabilityTheory.cauchyPDFReal_def', Orientation.neg_rotation_pi_div_two, ceil_pi_eq_four, cos_pi_div_thirty_two, Complex.sin_pi_div_two, NumberField.mixedEmbedding.polarSpaceCoord_target', Complex.sin_periodic, Complex.differentiable_on_off_countable_deriv_eq_smul_circleIntegral, Complex.cos_sub_pi_div_two, niven_angle_eq, Orientation.oangle_sub_left_smul_rotation_pi_div_two, Angle.two_zsmul_toReal_eq_two_mul_add_two_pi, Polynomial.Chebyshev.isMaxOn_T_real, integral_sqrt_one_sub_sq, cos_nat_mul_pi_sub, Polynomial.Chebyshev.rootMultiplicity_U_real, Orientation.oangle_add_right_smul_rotation_pi_div_two, Complex.arg_neg_one, Orientation.inner_smul_rotation_pi_div_two_left, surjOn_sin, sin_pi_div_thirty_two, Complex.tan_int_mul_pi_sub, tendsto_logDeriv_euler_cot_sub, neg_pi_div_two_lt_arcsin, hasSum_mellin_pi_mulβ, sin_pi_div_six, EulerSine.integral_cos_pow_eq, EuclideanGeometry.Sphere.oangle_eq_pi_sub_two_zsmul_oangle_center_right, image_tan_Ioo, sin_sub_pi, Angle.sin_eq_iff_eq_or_add_eq_pi, Complex.cos_int_mul_two_pi_sub_pi, Complex.cos_add_two_pi, pi_gt_d4, EuclideanGeometry.abs_oangle_left_toReal_lt_pi_div_two_of_dist_eq, Orientation.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq, hasDerivAt_fourierChar, pi_lt_sqrtTwoAddSeries, injOn_sin, Complex.toIocMod_arg, EisensteinSeries.q_expansion_bernoulli, Angle.coe_toIocMod, EuclideanGeometry.cos_eq_zero_iff_angle_eq_pi_div_two, hasDerivAt_Gamma_one_half, EuclideanGeometry.angle_left_midpoint_eq_pi_div_two_of_dist_eq, NumberField.mixedEmbedding.volume_eq_two_pow_mul_two_pi_pow_mul_integral, HurwitzZeta.hasSum_int_oddKernel, Angle.sign_add_pi, Gamma_mul_Gamma_add_half_of_pos, Complex.abs_arg_lt_pi_div_two_iff, HurwitzZeta.sinZeta_two_mul_nat_add_one, lt_sin_mul, Angle.abs_toReal_coe_eq_self_iff, NumberField.exists_ideal_in_class_of_norm_le, EulerSine.tendsto_integral_cos_pow_mul_div, EuclideanSpace.volume_ball_fin_two, Polynomial.fourierCoeff_toAddCircle_natCast, InnerProductGeometry.norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two, cos_nat_mul_two_pi_sub, norm_jacobiThetaβ'_term_le, completedRiemannZetaβ_one, fourierCoeffOn_of_hasDerivAt_Ioo, tendsto_tan_neg_pi_div_two, cos_pi_over_two_pow, NumberField.Ideal.tendsto_norm_le_div_atTop, Angle.toIocMod_toReal, Complex.circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable_of_tendsto, SchwartzMap.lineDerivOp_fourierInv_eq, tan_int_mul_pi_sub, EuclideanSpace.volume_ball, fourierChar_apply, Orientation.inner_eq_zero_iff_eq_zero_or_eq_smul_rotation_pi_div_two, Angle.sign_coe_pi_div_two, Angle.zsmul_eq_iff, Orientation.oangle_add_cyc3_neg_left, Circle.exp_int_mul_two_pi, GaussianFourier.integral_cexp_neg_mul_sq_add_real_mul_I, Polynomial.Chebyshev.sumZeroes_T_zero, GaussianFourier.integral_cexp_neg_mul_sum_add, arccos_of_le_neg_one, ModularFormClass.qExpansion_coeff_eq_circleIntegral, Angle.eq_neg_self_iff, tendsto_arctan_atTop, isAlgebraic_sin_rat_mul_pi, surjOn_cos, fourierIntegral_gaussian, HurwitzKernelBounds.F_nat_zero_zero_sub_le, quadratic_root_cos_pi_div_five, cos_antiperiodic, cos_periodic, Complex.arg_inv, Complex.sin_add_int_mul_two_pi, HurwitzZeta.hurwitzZeta_one_sub, NumberField.exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr, integral_gaussian_sq_complex, pi_gt_three, DiffContOnCl.two_pi_i_inv_smul_circleIntegral_sub_inv_smul, Orientation.eq_zero_or_oangle_eq_iff_inner_eq_zero, Complex.sin_pi, Sbtw.angleβββ_eq_pi, Angle.neg_coe_pi, EuclideanGeometry.abs_oangle_toReal_lt_pi_div_two_of_angle_eq_pi_div_two, Complex.exp_pi_mul_I, pi_lt_d20, Complex.isPrimitiveRoot_exp_rat_of_odd_num, Complex.tan_add_int_mul_pi, cos_sub_nat_mul_pi, two_mul_arctan_sub_pi, tan_pi_div_three, Complex.isIntegral_two_mul_cos_rat_mul_pi, pi_div_two_le_arcsin, arccos_lt_pi_div_two, sin_add_nat_mul_two_pi, Complex.Gammaβ_one_sub_mul_Gammaβ_one_add, Complex.tan_add_nat_mul_pi, tan_eq_zero_iff, arccos_neg_one, Complex.circleTransformDeriv_periodic, Circle.surjOn_exp_neg_pi_pi, EuclideanGeometry.angle_midpoint_eq_pi, hasSum_one_div_nat_pow_mul_sin, Polynomial.Chebyshev.roots_T_real, mul_lt_sin, tendsto_arctan_atBot, Complex.exp_sub_pi_mul_I, SchwartzMap.fderivCLM_fourier_eq, two_mul_arctan_add_pi, Angle.neg_eq_self_iff, pow_mul_norm_iteratedFDeriv_fourierIntegral_le, abs_sin_eq_one_iff, Complex.tan_eq_zero_iff, Complex.Gammaβ_add_two, Angle.cos_pos_iff_abs_toReal_lt_pi_div_two, mapsTo_sin_Ioo, circleIntegral.norm_integral_le_of_norm_le_const', floor_pi_eq_three, EuclideanGeometry.Sphere.two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi, Angle.coe_toIcoMod, euler_sineTerm_tprod, hasSum_zeta_two, sin_eq_neg_one_iff, EuclideanGeometry.angle_add_angle_eq_pi_of_angle_eq_pi, sin_pi_div_sixteen, EuclideanGeometry.collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi, two_mul_arctan_inv_3_add_arctan_inv_7, circleAverage_eq_intervalAverage, NumberField.abs_discr_ge_of_isTotallyComplex, Angle.cos_neg_iff_pi_div_two_lt_abs_toReal, cos_add_pi_div_two, arctan_inv_of_pos, tendsto_sum_pi_div_four, fourierChar_apply', Angle.tan_coe_pi, cos_sub_two_pi, Angle.cos_pi_div_two_sub, integral_sin_pow_succ_le, EuclideanGeometry.oangle_self_orthogonalProjection, Complex.exp_rat_mul_pi_mul_I_pow_two_mul_den, cos_int_mul_two_pi_sub_pi, circleIntegrable_def, VectorFourier.fourierPowSMulRight_apply, sin_sub_nat_mul_pi, strictConcaveOn_sin_Icc, pi_gt_d20, EisensteinSeries.G2_eq_tsum_cexp, integral_gaussian, arcsin_lt_pi_div_two, tan_sub_nat_mul_pi, Function.Periodic.norm_qParam, Complex.circleIntegral_one_div_sub_center_pow_smul_of_differentiable_on_off_countable, arctan_lt_pi_div_two, Complex.sin_sub_pi, EisensteinSeries.qExpansion_identity, Circle.argPartialEquiv_target, Polynomial.Chebyshev.eval_T_real_eq_one_iff, GaussianFourier.integral_cexp_neg_sum_mul_add, arctan_sqrt_three, Complex.cos_pi_div_two_sub, EuclideanGeometry.pi_div_three_lt_angle_of_le_of_le_of_ne, tsum_eisSummand_eq_tsum_sigma_mul_cexp_pow, cos_eq_one_iff, rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar_val, Complex.integral_rpow_mul_exp_neg_mul_rpow, EulerSine.integral_cos_pow_pos, HurwitzZeta.hasSum_int_sinZeta, sin_sq_pi_over_two_pow, sq_sin_pi_div_three, ZMod.toCircle_intCast, iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum, ZMod.toCircle_natCast, deriv_fourierChar, jacobiTheta_eq_tsum_nat, Complex.neg_pi_div_two_le_arg_iff, EuclideanGeometry.Sphere.IsTangentAt_iff_angle_eq_pi_div_two, monotoneOn_sin, cos_nat_mul_two_pi_add_pi, Complex.hasDerivAt_Gamma_one_half, Orientation.oangle_smul_add_right_eq_zero_or_eq_pi_iff, Angle.coe_two_pi, tendsto_integral_gaussian_smul, Complex.sin_sub_int_mul_two_pi, bernoulliFourierCoeff_recurrence, sin_nat_mul_pi_sub, arcsin_image_Icc, Complex.Gamma_mul_Gamma_add_half, EisensteinSeries.tendsto_tsum_one_div_linear_sub_succ_eq, sin_eq_zero_iff, tendsto_abs_tan_atTop, Complex.sin_two_pi_sub, Angle.eq_add_pi_of_two_zsmul_eq_of_sign_eq_neg, cos_sub_int_mul_two_pi, VectorFourier.norm_fourierSMulRight_le, EuclideanGeometry.angle_lt_pi_div_three_of_le_of_le_of_ne, HurwitzZeta.sinKernel_def, irrational_cos_rat_mul_pi, Complex.arg_ofReal_of_neg, neg_pi_div_two_le_arcsin, EuclideanGeometry.angle_self_orthogonalProjection, fourier_coe_apply', NumberField.abs_discr_rpow_ge_of_isTotallyComplex, TemperedDistribution.lineDerivOp_fourierInv_eq, HurwitzKernelBounds.F_nat_zero_le, Orientation.abs_oangle_sub_left_toReal_lt_pi_div_two, integral_sin_pow_odd, strictAntiOn_cos, Angle.nsmul_toReal_eq_mul, VectorFourier.norm_fourierPowSMulRight_le, integral_gaussian_complex, summable_pow_mul_jacobiThetaβ_term_bound, Angle.abs_toReal_add_abs_toReal_eq_pi_of_two_nsmul_add_eq_zero_of_sign_eq, hasFDerivAt_fourierChar_neg_bilinear_right, summable_bernoulli_fourier, Orientation.rotation_pi_div_two, VectorFourier.norm_fourierSMulRight, ZMod.toCircle_apply, InnerProductSpace.volume_closedBall, cos_int_mul_two_pi_sub, circleIntegral.integral_sub_center_inv, Complex.isAlgebraic_tan_rat_mul_pi, completedRiemannZeta_one, EuclideanGeometry.angle_right_midpoint_eq_pi_div_two_of_dist_eq, Orientation.oangle_eq_pi_iff_sameRay_neg, SchwartzMap.fourier_fderivCLM_eq, EuclideanGeometry.angle_pointReflection_right, Complex.Gammaβ_div_Gammaβ_one_sub, iteratedDeriv_fourierIntegral, InnerProductSpace.volume_closedBall_of_dim_odd, tendsto_euler_sin_prod, cosPartialEquiv_source, sin_pi_div_eight, Complex.cos_eq_neg_one_iff, Complex.Gamma_mul_Gamma_one_sub, Complex.arg_eq_nhds_of_re_neg_of_im_pos, arctan_eq_pi_div_four, integral_Ioi_inv_one_add_sq, Complex.log_neg_I, Complex.volume_sum_rpow_lt_one, rpow_def_of_nonpos, jacobiThetaβ_add_left', hasSum_one_div_pow_mul_fourier_mul_bernoulliFun, Polynomial.Chebyshev.integral_eval_T_real_mul_self_measureT_zero, Angle.abs_toReal_add_eq_two_pi_sub_abs_toReal_add_abs_toReal, NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr, Polynomial.Chebyshev.isLocalExtr_T_real, NumberField.Ideal.tendsto_norm_le_and_mk_eq_div_atTop, Complex.exp_two_pi_mul_I, Complex.arg_exp, Complex.tendsto_log_nhdsWithin_im_nonneg_of_re_neg_of_im_zero, EuclideanGeometry.Sphere.angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter, tan_add_nat_mul_pi, IsPrimitiveRoot.arg, tendsto_sin_pi_div_two, Angle.cos_sub_pi_div_two, arccos_zero, Polynomial.Chebyshev.isExtrOn_T_real, Orientation.inner_smul_rotation_pi_div_two_smul_left, Polynomial.instTwoPiPos, integral_gaussian_Ioi, arctan_add_eq_sub_pi, Circle.exp_eq_one, strictMonoOn_sin, Polynomial.toAddCircle_X_eq_fourier_one, EuclideanGeometry.oangle_eq_pi_iff_oangle_rev_eq_pi, unitary.norm_argSelfAdjoint_le_pi, Orientation.inner_smul_rotation_pi_div_two_smul_right, Angle.two_zsmul_eq_zero_iff, CircleIntegrable.out, Angle.toReal_le_pi, hasDerivAt_fourierIntegral, Complex.cos_nat_mul_two_pi_sub, cos_add_nat_mul_two_pi, Affine.Simplex.Equilateral.angle_eq_pi_div_three, fourierCoeffOn_of_hasDerivAt, Angle.two_nsmul_neg_pi_div_two, Complex.image_exp_Ioc_eq_sphere, CuspFormClass.exp_decay_atImInfty, InnerProductGeometry.angle_eq_pi_iff, Unitary.norm_argSelfAdjoint_le_pi, Complex.two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable, Angle.tan_add_pi, Angle.toReal_coe_eq_self_add_two_pi_iff, Complex.exp_eq_one_iff, Complex.cos_nat_mul_two_pi_add_pi, Complex.inv_Gammaβ_one_sub, Angle.sin_antiperiodic, DifferentiableOn.circleIntegral_one_div_sub_center_pow_smul, strictMonoOn_tan, Complex.exp_mul_I_antiperiodic, integral_Iic_inv_one_add_sq, Complex.arg_eq_nhds_of_re_neg_of_im_neg, isIntegral_two_mul_cos_rat_mul_pi, cos_eq_neg_one_iff, abs_cos_eq_one_iff, Complex.isAlgebraic_cos_rat_mul_pi, Complex.log_im_le_pi, sin_sub_two_pi, HurwitzZeta.hasSum_int_completedCosZeta, TorusIntegrable.function_integrable, NumberField.mixedEmbedding.volume_eq_two_pi_pow_mul_integral, EuclideanGeometry.two_zsmul_oangle_orthogonalProjection_self, Stirling.tendsto_stirlingSeq_sqrt_pi, HurwitzZeta.LSeriesHasSum_sin, hasStrictFDerivAt_rpow_of_neg, Complex.arg_mul_cos_add_sin_mul_I_sub, Angle.two_nsmul_coe_pi, cos_pi_div_three, Complex.cos_two_pi_sub, le_sin_mul, riemannZeta_two_mul_nat, Angle.toReal_eq_pi_div_two_iff, ModularForm.logDeriv_qParam, NumberField.mixedEmbedding.polarCoordReal_target, hasSum_zeta_nat, sin_add_pi, tendsto_euler_sin_prod', cos_add_int_mul_pi, Complex.polarCoord_target, Angle.toReal_coe_eq_self_sub_two_pi_iff, AddChar.zmod_intCast, surjOn_tan, arcsin_eq_neg_pi_div_two, HurwitzZeta.hurwitzZetaOdd_one_sub, Angle.sin_eq_real_sin_iff_eq_or_add_eq_pi, sin_sub_int_mul_two_pi, HurwitzZeta.hasSum_int_completedSinZeta, fourierInv_eq', fourierIntegral_deriv, Complex.tan_periodic, Polynomial.toAddCircle_C_eq_smul_fourier_zero, EuclideanGeometry.Sphere.angle_eq_pi_div_two_iff_mem_sphere_ofDiameter, Angle.cos_antiperiodic, Orientation.rotation_pi, Complex.sin_add_nat_mul_two_pi, cos_sub_pi_div_two, strictConcaveOn_cos_Icc, EuclideanGeometry.angle_lt_pi_of_not_collinear, AddCircle.homeomorphCircle'_apply, injOn_cos, EuclideanGeometry.angle_self_left, Complex.exp_mul_I_periodic, sin_eq_one_iff, tan_pi, HurwitzZeta.hasSum_nat_cosKernelβ, InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two, Angle.sin_sub_pi_div_two, cos_nat_mul_two_pi, Circle.exp_sub_two_pi, Complex.cos_eq_cos_iff, Polynomial.fourierCoeff_toAddCircle, TemperedDistribution.lineDeriv_eq_fourierMultiplierCLM, summable_pow_mul_cexp, sin_add_int_mul_two_pi, HurwitzZeta.sinZeta_one_sub, tendsto_prod_pi_div_two, Polynomial.Chebyshev.roots_U_real_nodup, Orientation.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero, Angle.tan_periodic, cos_pi, tan_sub_int_mul_pi, Angle.coe_pi_add_coe_pi, summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp, Complex.inv_Gammaβ_two_sub, VectorFourier.norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le, fderiv_fourierChar_neg_bilinear_left_apply, Complex.Gamma_one_half_eq, cos_int_mul_pi, Polynomial.Chebyshev.roots_T_real_nodup, cos_pi_div_two_sub, fourier_eq', Complex.cos_int_mul_two_pi, integral_sin_pow_antitone, Complex.arg_neg_eq_arg_sub_pi_iff, InnerProductSpace.volume_ball_of_dim_even, Complex.cos_two_pi, EuclideanSpace.volume_closedBall, Complex.cos_add_int_mul_two_pi, Angle.toReal_eq_neg_pi_div_two_iff, Orientation.oangle_add_cyc3_neg_right, fourierCoeffOn_of_hasDeriv_right, Complex.arg_I, sin_le_mul, Complex.arg_eq_pi_iff, Complex.exp_int_mul_two_pi_mul_I, Complex.arg_cos_add_sin_mul_I_eq_toIocMod, Circle.argEquiv_apply_coe, round_pi_eq_three, EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two, Complex.log_exp_exists, four_mul_arctan_inv_5_sub_arctan_inv_239, fourier_gaussian_pi, IsPrimitiveRoot.arg_eq_pi_iff, EuclideanGeometry.angle_add_angle_add_angle_eq_pi, ZMod.toCircle_eq_circleExp, Polynomial.Chebyshev.roots_U_real, deriv_fourier, Angle.two_nsmul_eq_iff, pi_gt_d6, tan_eq_zero_iff', Complex.arg_eq_neg_pi_div_two_iff, EulerSine.integral_cos_mul_cos_pow_even, integral_sin_pow_even, Angle.two_nsmul_toReal_eq_two_mul, SchwartzMap.laplacian_eq_fourierMultiplierCLM, Angle.sign_coe_neg_pi_div_two, EuclideanGeometry.angle_rev_eq_pi_div_two_of_oangle_eq_neg_pi_div_two, Complex.Gammaβ_one, pi_lt_d4, Angle.sign_antiperiodic, EuclideanGeometry.angle_eq_pi_iff_sbtw, hasSum_L_function_mod_four_eval_three, Complex.cos_pi, Orientation.abs_oangle_sub_right_toReal_lt_pi_div_two, Polynomial.Chebyshev.abs_eval_T_real_eq_one_iff, fourierIntegral_gaussian_pi', Function.Periodic.exp_decay_sub_of_bounded_at_inf, sin_int_mul_pi, integral_gaussian_complex_Ioi, log_doublingGamma_eq, InnerProductGeometry.angle_neg_left, arcsin_one, Complex.arg_eq_pi_iff_lt_zero, Function.Periodic.exp_decay_of_zero_at_inf, Complex.sin_add_pi, EuclideanGeometry.angle_eq_pi_sub_angle_div_two_of_oangle_eq_of_sOppSide, coe_sinOrderIso_apply, Polynomial.Chebyshev.eval_T_real_cos_int_mul_pi_div, differentiableAt_iteratedDerivWithin_cexp, pi_mul_cot_pi_q_exp, Wallis.le_W, Angle.nsmul_eq_iff, sin_pi_div_four, Complex.cos_sub_int_mul_two_pi, norm_jacobiThetaβ_term_fderiv_le, Complex.sin_add_pi_div_two, GaussianFourier.integral_rexp_neg_mul_sq_norm, HurwitzZeta.hasSum_int_evenKernelβ, tan_add_pi, sin_sq_pi_over_two_pow_succ, Angle.sin_sub_pi, Complex.arg_neg_coe_angle, Complex.angle_exp_exp, Angle.cos_coe_pi, continuousOn_tan_Ioo, Polynomial.fourierCoeff_toAddCircle_eq_zero_of_lt_zero, arctan_add_eq_add_pi, sin_sub_nat_mul_two_pi, EisensteinSeries.tsum_symmetricIco_tsum_sub_eq
|