Commit 2022-12-09 01:22 d53ae162

View on Github →

port: Algebra.Order.Group.Abs (#896) a95b16cbade0f938fc24abd05412bde1e84bab9b

  • depends on: #895 Issues:
  • typeclass inference
  • the absolute value notation can't cope with nesting or leading minus signs.

Estimated changes

added theorem abs_abs
added theorem abs_add'
added theorem abs_add
added theorem abs_add_three
added theorem abs_by_cases
added theorem abs_choice
added theorem abs_eq
added theorem abs_eq_abs
added theorem abs_eq_max_neg
added theorem abs_eq_sup_inv
added theorem abs_eq_zero
added theorem abs_le'
added theorem abs_le
added theorem abs_le_abs
added theorem abs_le_abs_of_nonneg
added theorem abs_le_abs_of_nonpos
added theorem abs_le_max_abs_abs
added theorem abs_lt
added theorem abs_max_le_max_abs_abs
added theorem abs_min_le_max_abs_abs
added theorem abs_neg
added theorem abs_nonneg
added theorem abs_nonpos_iff
added theorem abs_of_neg
added theorem abs_of_nonneg
added theorem abs_of_nonpos
added theorem abs_of_pos
added theorem abs_pos
added theorem abs_pos_of_neg
added theorem abs_pos_of_pos
added theorem abs_sub
added theorem abs_sub_abs_le_abs_sub
added theorem abs_sub_comm
added theorem abs_sub_le
added theorem abs_sub_le_iff
added theorem abs_sub_lt_iff
added theorem abs_zero
added theorem add_abs_nonneg
added theorem eq_of_abs_sub_eq_zero
added theorem eq_of_abs_sub_nonpos
added theorem eq_or_eq_neg_of_abs_eq
added theorem le_abs'
added theorem le_abs
added theorem le_abs_self
added theorem le_of_abs_le
added theorem lt_abs
added theorem lt_of_abs_lt
added theorem max_sub_min_eq_abs'
added theorem max_sub_min_eq_abs
added theorem min_abs_abs_le_abs_max
added theorem min_abs_abs_le_abs_min
added theorem neg_abs_le_neg
added theorem neg_abs_le_self
added theorem neg_le_abs_self
added theorem neg_le_of_abs_le
added theorem neg_lt_of_abs_lt