Commit 2023-03-08 06:27 1a9e5d67

View on Github →

feat: port Data.Real.Sqrt (#2674)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Real/Sqrt.lean

added theorem Continuous.sqrt

added theorem ContinuousOn.sqrt

added theorem Filter.Tendsto.sqrt

added theorem NNReal.continuous_sqrt

added theorem NNReal.le_sqrt_iff

added theorem NNReal.mul_self_sqrt

added theorem NNReal.sq_sqrt

added theorem NNReal.sqrt_div

added theorem NNReal.sqrt_eq_iff_sq_eq

added theorem NNReal.sqrt_eq_zero

added theorem NNReal.sqrt_inv

added theorem NNReal.sqrt_le_iff

added theorem NNReal.sqrt_le_sqrt_iff

added theorem NNReal.sqrt_lt_sqrt_iff

added theorem NNReal.sqrt_mul

added theorem NNReal.sqrt_mul_self

added theorem NNReal.sqrt_one

added theorem NNReal.sqrt_sq

added theorem NNReal.sqrt_zero

added theorem Real.abs_le_sqrt

added theorem Real.coe_sqrt

added theorem Real.continuous_sqrt

added theorem Real.div_sqrt

added theorem Real.le_sqrt'

added theorem Real.le_sqrt

added theorem Real.le_sqrt_of_sq_le

added theorem Real.lt_sq_of_sqrt_lt

added theorem Real.lt_sqrt

added theorem Real.lt_sqrt_of_sq_lt

added theorem Real.mul_self_sqrt

added theorem Real.nat_sqrt_le_real_sqrt

added theorem Real.neg_sqrt_le_of_sq_le

added theorem Real.neg_sqrt_lt_of_sq_lt

added theorem Real.real_sqrt_le_nat_sqrt_succ

added theorem Real.sq_le

added theorem Real.sq_lt

added theorem Real.sq_sqrt

added def Real.sqrtAux

added theorem Real.sqrtAux_nonneg

added theorem Real.sqrt_div'

added theorem Real.sqrt_div

added theorem Real.sqrt_div_self'

added theorem Real.sqrt_div_self

added theorem Real.sqrt_eq_cases

added theorem Real.sqrt_eq_iff_mul_self_eq

added theorem Real.sqrt_eq_iff_mul_self_eq_of_pos

added theorem Real.sqrt_eq_iff_sq_eq

added theorem Real.sqrt_eq_one

added theorem Real.sqrt_eq_zero'

added theorem Real.sqrt_eq_zero

added theorem Real.sqrt_eq_zero_of_nonpos

added theorem Real.sqrt_inj

added theorem Real.sqrt_inv

added theorem Real.sqrt_le_iff

added theorem Real.sqrt_le_left

added theorem Real.sqrt_le_sqrt

added theorem Real.sqrt_le_sqrt_iff

added theorem Real.sqrt_lt'

added theorem Real.sqrt_lt

added theorem Real.sqrt_lt_sqrt

added theorem Real.sqrt_lt_sqrt_iff

added theorem Real.sqrt_lt_sqrt_iff_of_pos

added theorem Real.sqrt_mul'

added theorem Real.sqrt_mul

added theorem Real.sqrt_mul_self

added theorem Real.sqrt_mul_self_eq_abs

added theorem Real.sqrt_ne_zero'

added theorem Real.sqrt_ne_zero

added theorem Real.sqrt_nonneg

added theorem Real.sqrt_one

added theorem Real.sqrt_pos

added theorem Real.sqrt_sq

added theorem Real.sqrt_sq_eq_abs

added theorem Real.sqrt_zero