Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-01 18:24 ec611821

View on Github →

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

Estimated changes

Modified src/algebra/group_power/order.lean

added theorem one_le_sq_iff_one_le_abs

added theorem one_lt_sq_iff_one_lt_abs

added theorem sq_eq_one_iff

added theorem sq_eq_sq_iff_abs_eq_abs

added theorem sq_le_one_iff_abs_le_one

added theorem sq_lt_one_iff_abs_lt_one

modified theorem sq_lt_sq

added theorem sq_ne_one_iff

Modified src/analysis/inner_product_space/basic.lean