Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-03 17:44 360fa07e

View on Github →

feat(data/real/sqrt): added some missing sqrt lemmas (#5933) I noticed that some facts about sqrt and abs are missing, so I am adding them.

Estimated changes

deleted theorem abs_sq_eq
added theorem abs_sqr
added theorem sqr_abs
added theorem sqr_le_sqr'
added theorem sqr_le_sqr
added theorem sqr_lt_sqr'
added theorem sqr_lt_sqr
modified theorem abs_le'
modified theorem abs_le
modified theorem abs_lt
added theorem le_abs
added theorem le_of_abs_le
modified theorem lt_abs
added theorem lt_of_abs_lt
added theorem neg_le_of_abs_le
added theorem neg_lt_of_abs_lt
added theorem real.abs_le_sqrt
added theorem real.div_sqrt
modified theorem real.le_sqrt'
modified theorem real.le_sqrt
modified theorem real.le_sqrt_of_sqr_le
added theorem real.lt_sqrt
added theorem real.lt_sqrt_of_sqr_lt
added theorem real.sqr_le
added theorem real.sqr_lt
modified theorem real.sqrt_le_iff
modified theorem real.sqrt_le_left
modified theorem real.sqrt_le_sqrt
added theorem real.sqrt_ne_zero'
added theorem real.sqrt_ne_zero