sqrt 📖 | CompOp | 336 mathmath: Behrend.roth_lower_bound, arctan_eq_arccos, pi_div_four_le_arcsin, hasDerivAt_arccos, RCLike.sqrt_eq_ite, cos_pi_div_five, one_le_sqrt, sqrt_eq_iff_eq_sq, sin_arctan, sqrt_eq_cases, TsirelsonInequality.sqrt_two_inv_mul_self, hasDerivAt_sqrt_mul_log, arctan_eq_arcsin, sqrt_one_add_le, strictMonoOn_sqrt, Stirling.factorial_isEquivalent_stirling, DifferentiableOn.sqrt, dist_mulExpNegMulSq_le_two_mul_sqrt, real_sqrt_le_nat_sqrt_succ, log_sqrt, Gamma_nat_add_half, Chebyshev.abs_psi_sub_theta_le_sqrt_mul_log, RCLike.re_sqrt_ofReal, ProbabilityTheory.Fernique.lt_normThreshold_zero, NumberField.dedekindZeta_residue_def, nat_floor_real_sqrt_eq_nat_sqrt, InnerProductGeometry.sin_angle, DifferentiableWithinAt.sqrt, sqrt_div_self, Complex.re_sqrt_ofReal, add_sqrt_self_sq_sub_one_inv, Behrend.roth_lower_bound_explicit, neg_sqrt_lt_of_sq_lt, Complex.sqrt_I, Behrend.sphere_subset_preimage_metric_sphere, deriv_arccos, cos_le_one_div_sqrt_sq_add_one, ContDiffOn.sqrt, deriv_sqrt_mul_log, ContinuousWithinAt.sqrt, irrational_sqrt_ratCast_iff, Polynomial.Chebyshev.integral_measureT, sin_pi_div_three, Behrend.log_two_mul_two_le_sqrt_log_eight, hasDerivAt_arcosh, irrational_sqrt_intCast_iff, HasDerivAt.sqrt, cos_arcsin, tan_arccos, sinh_arcosh, hasStrictDerivAt_arccos, InnerProductSpace.Core.norm_eq_sqrt_re_inner, WithLp.prod_dist_eq_of_L2, sqrt_inv, Gamma_mul_Gamma_add_half, HasStrictFDerivAt.arsinh, NumberField.mixedEmbedding.exists_primitive_element_lt_of_isComplex, sqrt_monotone, PositiveLinearMap.preGNS_norm_def, UpperHalfPlane.dist_eq_iff_eq_sinh, norm_add_eq_sqrt_iff_real_inner_eq_zero, hasDerivAt_arsinh, le_sqrt', cos_pi_div_four, contDiffAt_sqrt, Tactic.NormNum.isNat_realSqrt, deriv_sqrt_aux, sqrt_sq_eq_abs, sqrt_mul_self, continuous_sqrt, cos_pi_div_sixteen, tanh_arcosh, Gamma_one_half_eq, strictConcaveOn_sqrt_mul_log_Ioi, exp_arcosh, irrational_sqrt_natCast_iff, hasDerivWithinAt_arccos_Ici, irrational_sqrt_ratCast_iff_of_nonneg, tan_div_sqrt_one_add_tan_sq, sqrt_le_iff, sqrt_lt_sqrt_iff_of_pos, sq_le, sqrt_two_lt_three_halves, Tactic.NormNum.isNNRat_realSqrt_of_isNNRat, abs_le_sqrt, sqrt_le_sqrt_iff, Stirling.stirlingSeq_one, HasDerivWithinAt.sqrt, Behrend.lower_bound_le_one, sqrt_div', real_sqrt_lt_nat_sqrt_succ, Behrend.norm_of_mem_sphere, UpperHalfPlane.dist_coe_center, norm_sub_eq_sqrt_iff_real_inner_eq_zero, sqrtTwoAddSeries_two, Stirling.le_factorial_stirling, coe_fib_eq, mul_self_sqrt, CStarModule.norm_eq_sqrt_norm_inner_self, sqrt_eq_zero_of_nonpos, le_sqrt_of_sq_le, Nat.realSqrt_mem_Ico, hasStrictDerivAt_arcosh, ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_right, dist_integral_mulExpNegMulSq_comp_le, HasStrictFDerivAt.sqrt, HasDerivWithinAt.arsinh, ContinuousAt.sqrt, DifferentiableAt.sqrt, hasDerivAt_arcsin, gold_sub_goldConj, arcsin_eq_arccos, irrational_sqrt_intCast_iff_of_nonneg, map_sqrt_atTop, arccos_le_pi_div_four, InnerProductSpace.volume_ball, sqrt_mul, cos_pi_div_eight, Complex.sqrt_of_nonneg, NumberField.mixedEmbedding.covolume_idealLattice, RCLike.sqrt_real, arccos_eq_arcsin, exp_arsinh, RCLike.sqrt_eq_real_add_ite, sq_sqrt, ProbabilityTheory.gaussianPDFReal_def, le_sqrt, sqrt_le_sqrt, floor_real_sqrt_eq_nat_sqrt, Complex.normSq_ofReal_add_I_mul_sqrt_one_sub, ProbabilityTheory.Fernique.normThreshold_eq, UpperHalfPlane.dist_eq, sqrt_div_self', comap_sqrt_atTop, WithCStarModule.pi_norm, Stirling.sqrt_pi_le_stirlingSeq, hasDerivWithinAt_arcsin_Ici, NumberField.Ideal.tendsto_norm_le_div_atTop₀, Asymptotics.IsBigO.sqrt, abs_sin_half, sqrtTwoAddSeries_succ, abs_sin_eq_sqrt_one_sub_cos_sq, sqrt_lt', cos_pi_div_six, sin_half_eq_neg_sqrt, sqrt_le_one, coe_intFib_eq, Gamma_nat_add_one_add_half, ContinuousOn.sqrt, hasStrictDerivAt_arsinh, RCLike.sqrt_of_nonneg, inv_sqrt_two_sub_one, sq_lt, sqrt_lt_sqrt_iff, irrational_sqrt_of_multiplicity_odd, Nat.realSqrt_lt_ratSqrt_add_inv_prec, Complex.cpow_inv_two_im_eq_sqrt, Complex.cpow_inv_two_re, pi_gt_sqrtTwoAddSeries, tsirelson_inequality, WithCStarModule.prod_norm, HasDerivAt.arsinh, log_div_sqrt_antitoneOn, EuclideanSpace.norm_eq, ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_left, arccos_eq_arctan, NumberField.mixedEmbedding.covolume_integerLattice, neg_sqrt_le_of_sq_le, exp_half, sin_pi_over_two_pow_succ, deriv_arcsin, div_sqrt, tan_pi_div_six, arctan_inv_sqrt_three, sqrt_pos, cos_pi_div_thirty_two, inv_sqrt_one_add_tan_sq, Complex.norm_def, sqrt_eq_iff_mul_self_eq, UpperHalfPlane.dist_le_dist_coe_div_sqrt, integral_sqrt_one_sub_sq, Complex.norm_add_mul_I, HasFDerivWithinAt.arsinh, sin_pi_div_thirty_two, sqrtTwoAddSeries_one, mulExpNegMulSq_eq_sqrt_mul_mulExpNegMulSq_one, sqrt_eq_iff_mul_self_eq_of_pos, sqrt_zero, lt_sqrt_of_sq_lt, sqrt_mul_self_eq_abs, pi_lt_sqrtTwoAddSeries, coe_fib_eq', hasDerivAt_Gamma_one_half, sqrt_pos_of_pos, HasStrictDerivAt.arsinh, Gamma_mul_Gamma_add_half_of_pos, sum_mul_le_sqrt_mul_sqrt, Complex.sqrt_neg_I, HasFDerivWithinAt.sqrt, NumberField.exists_ideal_in_class_of_norm_le, Complex.sqrt_eq_real_add_ite, Measurable.sqrt, fderivWithin_sqrt, RCLike.sqrt_neg_I, lt_sqrt, sin_arccos, NumberField.Ideal.tendsto_norm_le_div_atTop, UpperHalfPlane.cosh_half_dist, EuclideanSpace.volume_ball, sqrt_le_left, sq_sqrt', abs_cos_eq_sqrt_one_sub_sin_sq, OpenPartialHomeomorph.univUnitBall_apply, cos_half, RCLike.sqrt_I, Differentiable.sqrt, UpperHalfPlane.exp_half_dist, cosh_arsinh, strictConcaveOn_sqrt, NumberField.exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr, OrthonormalBasis.norm_le_card_mul_iSup_norm_inner, tan_pi_div_three, nat_sqrt_le_real_sqrt, hasStrictDerivAt_arcsin, Chebyshev.psi_le, HasFDerivAt.arsinh, cos_lt_one_div_sqrt_sq_add_one, sin_pi_div_sixteen, tendsto_sqrt_atTop, Asymptotics.IsLittleO.sqrt, UpperHalfPlane.sinh_half_dist_add_dist, Complex.dist_mk, derivWithin_sqrt, Tactic.NormNum.isNat_realSqrt_neg, polarCoord_apply, EuclideanSpace.dist_eq, exp_artanh, hasStrictDerivAt_sqrt, integral_gaussian, fderiv_sqrt, arctan_sqrt_three, sqrt_sq, Continuous.sqrt, Behrend.le_sqrt_log, PiLp.dist_eq_of_L2, ContDiff.sqrt, Complex.hasDerivAt_Gamma_one_half, Complex.Gamma_mul_Gamma_add_half, Complex.cpow_inv_two_im_eq_neg_sqrt, abs_mulExpNegMulSq_le, Filter.Tendsto.sqrt, goldenRatio_sub_goldenConj, Behrend.lower_bound_le_one', ProbabilityTheory.Fernique.sq_normThreshold_add_one_le, Asymptotics.IsTheta.sqrt, ProbabilityTheory.measure_le_mul_measure_gt_le_of_map_rotation_eq_self, rpow_div_two_eq_sqrt, InnerProductSpace.volume_closedBall, UpperHalfPlane.sinh_half_dist, UpperHalfPlane.dist_le_iff_le_sinh, sin_pi_div_eight, Bertrand.real_main_inequality, Nat.ratSqrt_mem_Ioc, sqrt_one, Zsqrtd.toReal_apply, sqrt_div, NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr, HasFDerivAt.sqrt, sqrt_nonneg, NumberField.Ideal.tendsto_norm_le_and_mk_eq_div_atTop, ruzsaSzemerediNumberNat_lower_bound, norm_eq_sqrt_re_inner, deriv_arcsin_aux, coe_sqrt, sqrt_lt, integral_gaussian_Ioi, Complex.norm_eq_sqrt_sq_add_sq, sqrt_mul', Nat.ratSqrt_le_realSqrt, abs_integral_sub_setIntegral_mulExpNegMulSq_comp_lt, AEMeasurable.sqrt, irrational_sqrt_ofNat_iff, RCLike.sqrt_normSq_eq_norm, Stirling.tendsto_stirlingSeq_sqrt_pi, arcsin_eq_arctan, ruzsaSzemerediNumberNat_asymptotic_lower_bound, cos_eq_sqrt_one_sub_sin_sq, tanh_arsinh, PiLp.norm_eq_of_L2, sum_sqrt_mul_sqrt_le, Complex.abs_cpow_inv_two_im, Nat.Prime.irrational_sqrt, Complex.norm_le_sqrt_two_mul_max, tan_arcsin, sqrt_one_add_norm_sq_le, InnerProductGeometry.sin_angle_add, Polynomial.Chebyshev.intervalIntegrable_sqrt_one_sub_sq_inv, CFC.sqrt_eq_real_sqrt, OpenPartialHomeomorph.univUnitBall_symm_apply, ProbabilityTheory.Fernique.normThreshold_add_one, one_lt_sqrt_two, sqrt_lt_sqrt, CFC.norm_sqrt, sqrt_eq_one, WithLp.prod_norm_eq_of_L2, hasDerivAt_sqrt, hasDerivWithinAt_arccos_Iic, deriv_sqrt_mul_log', sinh_artanh, InnerProductGeometry.sin_angle_mul_norm_mul_norm, EuclideanSpace.volume_closedBall, sqrt_eq_rpow, sin_half_eq_sqrt, sin_eq_sqrt_one_sub_cos_sq, sqrt_eq_zero', Complex.normSq_ofReal_sub_I_mul_sqrt_one_sub, sqrt_inj, Tactic.NormNum.isNat_realSqrt_of_isRat_negOfNat, irrational_sqrt_two, cosh_artanh, ContDiffWithinAt.sqrt, ContDiffAt.sqrt, sqrt_prod, HasStrictDerivAt.sqrt, hasDerivWithinAt_arcsin_Iic, InnerProductSpace.Core.sqrt_normSq_eq_norm, sqrt_eq_zero, log_doublingGamma_eq, deriv_sqrt, deriv2_sqrt_mul_log, sin_pi_div_four, sqrt_le_sqrt_iff', Complex.dist_eq_re_im, cos_arctan, norm_eq_sqrt_real_inner, one_add_norm_le_sqrt_two_mul_sqrt
|