Mathlib v3 is deprecated. Go to Mathlib v4

Theorem one_lt_sq_iff_one_lt_abs

Modification history

2022-02-01 18:24

src/algebra/group_power/order.lean

feat(algebra/group_power): relate square equality and absolute value equality (#11683)

Added one_lt_sq_iff_one_lt_abs View on Github →