Commit 2022-06-03 16:16 2a21a861
View on Github →refactor(algebra/order/ring): turn sq_le_sq into an iff (#14511)
sq_le_sqandsq_lt_sqare nowifflemmas;- drop
abs_le_abs_of_sq_le_sqandabs_lt_abs_of_sq_lt_sq.
refactor(algebra/order/ring): turn sq_le_sq into an iff (#14511)
sq_le_sq and sq_lt_sq are now iff lemmas;abs_le_abs_of_sq_le_sq and abs_lt_abs_of_sq_lt_sq.