Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-29 04:56 6de241f9

View on Github →

feat(data/rat/nnrat): Nonnegative rationals (#16283) Define nnrat, the subtype of nonnegative rational numbers, and show it forms a canonically_linear_ordered_semifield.

Estimated changes

added theorem nnrat.abs_coe
added theorem nnrat.bdd_above_coe
added theorem nnrat.bdd_below_coe
added theorem nnrat.coe_add
added theorem nnrat.coe_bit0
added theorem nnrat.coe_bit1
added theorem nnrat.coe_coe_hom
added theorem nnrat.coe_div
added theorem nnrat.coe_eq_zero
added def nnrat.coe_hom
added theorem nnrat.coe_indicator
added theorem nnrat.coe_inj
added theorem nnrat.coe_inv
added theorem nnrat.coe_le_coe
added theorem nnrat.coe_list_prod
added theorem nnrat.coe_list_sum
added theorem nnrat.coe_lt_coe
added theorem nnrat.coe_max
added theorem nnrat.coe_min
added theorem nnrat.coe_mk
added theorem nnrat.coe_mono
added theorem nnrat.coe_mul
added theorem nnrat.coe_multiset_sum
added theorem nnrat.coe_nat_cast
added theorem nnrat.coe_ne_zero
added theorem nnrat.coe_nonneg
added theorem nnrat.coe_one
added theorem nnrat.coe_pos
added theorem nnrat.coe_pow
added theorem nnrat.coe_prod
added theorem nnrat.coe_sub
added theorem nnrat.coe_sum
added theorem nnrat.coe_zero
added def nnrat.denom
added theorem nnrat.denom_coe
added theorem nnrat.ext
added theorem nnrat.ext_iff
added theorem nnrat.ext_num_denom
added theorem nnrat.mk_coe_nat
added theorem nnrat.nat_abs_num_coe
added theorem nnrat.ne_iff
added theorem nnrat.nsmul_coe
added def nnrat.num
added theorem nnrat.num_div_denom
added theorem nnrat.sub_def
added theorem nnrat.to_nnrat_coe
added theorem nnrat.to_nnrat_coe_nat
added theorem nnrat.to_nnrat_mono
added theorem nnrat.val_eq_coe
added def nnrat
added theorem rat.coe_nnabs
added theorem rat.coe_to_nnrat
added theorem rat.le_coe_to_nnrat
added def rat.nnabs
added def rat.to_nnrat
added theorem rat.to_nnrat_add
added theorem rat.to_nnrat_add_le
added theorem rat.to_nnrat_bit0
added theorem rat.to_nnrat_bit1
added theorem rat.to_nnrat_div'
added theorem rat.to_nnrat_div
added theorem rat.to_nnrat_eq_zero
added theorem rat.to_nnrat_inv
added theorem rat.to_nnrat_mul
added theorem rat.to_nnrat_one
added theorem rat.to_nnrat_pos
added theorem rat.to_nnrat_zero