Mathlib v3 is deprecated. Go to Mathlib v4

Theorem abs_le_abs_of_sqr_le_sqr

Modification history

2021-04-28 19:37
src/algebra/group_power/basic.lean
chore(*): use `sq` as convention for "squared" (#7368) …
Deleted abs_le_abs_of_sqr_le_sqrView on Github →
2021-02-22 03:13
src/algebra/group_power/basic.lean
feat(algebra/group_power/basic): `abs_lt_abs_of_sqr_lt_sqr` (#6277) …
Added abs_le_abs_of_sqr_le_sqrView on Github →