Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-22 03:13 2134d0c1

View on Github →

feat(algebra/group_power/basic): abs_lt_abs_of_sqr_lt_sqr (#6277) These lemmas are (almost) the converses of some of the lemmas I added in #5933.

Estimated changes

added theorem abs_le_of_sqr_le_sqr'
added theorem abs_le_of_sqr_le_sqr
added theorem abs_lt_of_sqr_lt_sqr'
added theorem abs_lt_of_sqr_lt_sqr
modified theorem abs_sqr
modified theorem sqr_abs