Commit 2023-02-21 07:40 d6aef3a9

View on Github →

feat: port Data.Rat.NNRat (#2392)

Estimated changes

added theorem NNRat.abs_coe
added theorem NNRat.bddAbove_coe
added theorem NNRat.bddBelow_coe
added def NNRat.coeHom
added theorem NNRat.coe_add
added theorem NNRat.coe_coeHom
added theorem NNRat.coe_div
added theorem NNRat.coe_eq_zero
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.den
added theorem NNRat.den_coe
added theorem NNRat.ext
added theorem NNRat.ext_iff
added theorem NNRat.ext_num_den
added theorem NNRat.ext_num_den_iff
added theorem NNRat.mk_coe_nat
added theorem NNRat.natAbs_num_coe
added theorem NNRat.ne_iff
added theorem NNRat.nsmul_coe
added def NNRat.num
added theorem NNRat.num_div_den
added theorem NNRat.sub_def
added theorem NNRat.toNNRat_coe
added theorem NNRat.toNNRat_coe_nat
added theorem NNRat.toNNRat_mono
added def NNRat
added theorem Rat.coe_nnabs
added theorem Rat.coe_toNNRat
added theorem Rat.le_coe_toNNRat
added def Rat.nnabs
added def Rat.toNNRat
added theorem Rat.toNNRat_add
added theorem Rat.toNNRat_add_le
added theorem Rat.toNNRat_div'
added theorem Rat.toNNRat_div
added theorem Rat.toNNRat_eq_zero
added theorem Rat.toNNRat_inv
added theorem Rat.toNNRat_mul
added theorem Rat.toNNRat_one
added theorem Rat.toNNRat_pos
added theorem Rat.toNNRat_zero