Mathlib v3 is deprecated. Go to Mathlib v4

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

added theorem mul_sub'
added theorem sub_mul'
added theorem add_hom.le_map_sub
added theorem le_mul_sub
added theorem le_sub_mul
added theorem order_iso.map_sub
added def add_hom.mul_left
added theorem bool.cond_bnot
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