Commit 2021-09-15 18:42 8185637f

View on Github →

refactor(data/real/nnreal): use has_ordered_sub (#9167)

  • provide a has_ordered_sub instance for nnreal;
  • drop most lemmas about subtraction in favor of lemmas from algebra/ordered_sub;
  • add mul_sub' and sub_mul';
  • generalize some lemmas about has_ordered_sub to has_add;
  • add add_hom.mul_left and add_hom.mul_right.

Estimated changes

deleted theorem nnreal.add_sub_cancel'
deleted theorem nnreal.add_sub_cancel
deleted theorem nnreal.add_sub_eq_max
added theorem nnreal.coe_sub_def
deleted theorem nnreal.lt_sub_iff_add_lt
deleted theorem nnreal.sub_add_eq_max
added theorem nnreal.sub_div
deleted theorem nnreal.sub_eq_iff_eq_add
deleted theorem nnreal.sub_eq_zero
deleted theorem nnreal.sub_le_iff_le_add
deleted theorem nnreal.sub_le_self
deleted theorem nnreal.sub_lt_iff_lt_add
deleted theorem nnreal.sub_pos
deleted theorem nnreal.sub_self
deleted theorem nnreal.sub_zero