Commit 2024-04-13 10:35 8640948c

View on Github →

feat: add notation for Real.sqrt (#12056) This adds the notation √r for Real.sqrt r. The precedence is such that √x⁻¹ is parsed as √(x⁻¹); not because this is particularly desirable, but because it's the default and the choice doesn't really matter. This is extracted from #7907, which adds a more general nth root typeclass. The idea is to perform all the boring substitutions downstream quickly, so that we can play around with custom elaborators with a much slower rate of code-rot. This PR also won't rot as quickly, as it does not forbid writing x.sqrt as that PR does. While perhaps claiming √ for Real.sqrt is greedy; it:

  • Is far more common thatn NNReal.sqrt and Nat.sqrt
  • Is far more interesting to mathlib than sqrt on Float
  • Can be overloaded anyway, so this does not prevent downstream code using the notation on their own types.
  • Will be replaced by a more general typeclass in a future PR. Zulip

Estimated changes

modified theorem Complex.dist_eq_re_im
modified theorem UpperHalfPlane.dist_eq
modified theorem Real.strictConcaveOn_sqrt
modified theorem norm_eq_sqrt_inner
modified theorem norm_eq_sqrt_real_inner
modified theorem RCLike.sqrt_normSq_eq_norm
modified theorem Real.cosh_arsinh
modified theorem Real.exp_arsinh
modified theorem Real.hasDerivAt_arsinh
modified theorem Real.exp_half
modified theorem Real.Gamma_one_half_eq
modified theorem integral_gaussian
modified theorem integral_sqrt_one_sub_sq
modified theorem sqrt_one_add_norm_sq_le
modified theorem Real.log_sqrt
modified theorem Real.rpow_div_two_eq_sqrt
modified theorem Real.sqrt_eq_rpow
modified theorem ContDiff.sqrt
modified theorem Real.contDiffAt_sqrt
modified theorem Real.hasDerivAt_sqrt
modified theorem Real.hasStrictDerivAt_sqrt
modified theorem Stirling.stirlingSeq_one
modified theorem Real.arccos_eq_arctan
modified theorem Real.arctan_eq_arccos
modified theorem Real.arctan_eq_arcsin
modified theorem Real.cos_arctan
modified theorem Real.sin_arctan
modified theorem Real.cos_pi_div_eight
modified theorem Real.cos_pi_div_four
modified theorem Real.cos_pi_div_six
modified theorem Real.cos_pi_div_sixteen
modified theorem Real.cos_pi_div_thirty_two
modified theorem Real.sin_pi_div_eight
modified theorem Real.sin_pi_div_four
modified theorem Real.sin_pi_div_sixteen
modified theorem Real.sin_pi_div_thirty_two
modified theorem Real.sin_pi_div_three
modified theorem Real.sqrtTwoAddSeries_one
modified theorem Real.sqrtTwoAddSeries_two
modified theorem Real.arccos_eq_arcsin
modified theorem Real.arccos_le_pi_div_four
modified theorem Real.arcsin_eq_arccos
modified theorem Real.cos_arcsin
modified theorem Real.pi_div_four_le_arcsin
modified theorem Real.sin_arccos
modified theorem Real.tan_arccos
modified theorem Real.tan_arcsin
modified theorem Real.deriv_arccos
modified theorem Real.deriv_arcsin
modified theorem Behrend.le_sqrt_log
modified theorem Behrend.roth_lower_bound
modified theorem Real.coe_fib_eq
modified theorem gold_sub_goldConj
modified def goldenConj
modified def goldenRatio
modified theorem Nat.Prime.irrational_sqrt
modified theorem irrational_sqrt_two
modified theorem Continuous.sqrt
modified theorem ContinuousOn.sqrt
modified theorem Real.abs_le_sqrt
modified theorem Real.coe_sqrt
modified theorem Real.continuous_sqrt
modified theorem Real.div_sqrt
modified theorem Real.le_sqrt'
modified theorem Real.le_sqrt
modified theorem Real.le_sqrt_of_sq_le
modified theorem Real.lt_sq_of_sqrt_lt
modified theorem Real.lt_sqrt
modified theorem Real.lt_sqrt_of_sq_lt
modified theorem Real.mul_self_sqrt
modified theorem Real.nat_sqrt_le_real_sqrt
modified theorem Real.neg_sqrt_le_of_sq_le
modified theorem Real.neg_sqrt_lt_of_sq_lt
modified theorem Real.one_le_sqrt
modified theorem Real.sq_le
modified theorem Real.sq_lt
modified theorem Real.sq_sqrt
modified theorem Real.sqrt_div'
modified theorem Real.sqrt_div
modified theorem Real.sqrt_div_self'
modified theorem Real.sqrt_div_self
modified theorem Real.sqrt_eq_cases
modified theorem Real.sqrt_eq_iff_sq_eq
modified theorem Real.sqrt_eq_one
modified theorem Real.sqrt_eq_zero'
modified theorem Real.sqrt_eq_zero
modified theorem Real.sqrt_inj
modified theorem Real.sqrt_inv
modified theorem Real.sqrt_le_iff
modified theorem Real.sqrt_le_left
modified theorem Real.sqrt_le_one
modified theorem Real.sqrt_le_sqrt
modified theorem Real.sqrt_le_sqrt_iff'
modified theorem Real.sqrt_le_sqrt_iff
modified theorem Real.sqrt_lt'
modified theorem Real.sqrt_lt
modified theorem Real.sqrt_lt_sqrt
modified theorem Real.sqrt_lt_sqrt_iff
modified theorem Real.sqrt_mul'
modified theorem Real.sqrt_mul
modified theorem Real.sqrt_mul_self
modified theorem Real.sqrt_mul_self_eq_abs
modified theorem Real.sqrt_ne_zero'
modified theorem Real.sqrt_ne_zero
modified theorem Real.sqrt_nonneg
modified theorem Real.sqrt_one
modified theorem Real.sqrt_one_add_le
modified theorem Real.sqrt_pos
modified theorem Real.sqrt_sq
modified theorem Real.sqrt_sq_eq_abs
modified theorem Real.sqrt_zero
modified theorem Measurable.sqrt
modified theorem isBigO_zero_zetaKernel₂