Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-01 05:10 370cc484

View on Github →

chore(data/real/nnreal): Golf (#16307) Generalize various lemmas to linear_ordered_semifield or weaker so that they apply to nnreal. Golf the nnreal API using them.

Estimated changes

modified theorem finset.sum_div
added theorem two_inv_lt_one
modified theorem nnreal.add_halves
modified theorem nnreal.div_add_div_same
modified theorem nnreal.div_le_iff
modified theorem nnreal.div_pos
modified theorem nnreal.div_self_le
modified theorem nnreal.half_le_self
modified theorem nnreal.half_lt_self
modified theorem nnreal.half_pos
modified theorem nnreal.inv_lt_inv_iff
modified theorem nnreal.inv_lt_one
modified theorem nnreal.inv_pos
modified theorem nnreal.le_div_iff_mul_le
modified theorem nnreal.sub_div
modified theorem nnreal.two_inv_lt_one