Commit 2023-02-11 09:23 dbaddcee

View on Github →

feat: port Algebra.Order.Nonneg.Ring (#1260) Really difficult to diagnose timeout here

Estimated changes

added theorem Nonneg.bot_eq
added theorem Nonneg.coe_toNonneg
added theorem Nonneg.mk_add_mk
added theorem Nonneg.mk_eq_one
added theorem Nonneg.mk_eq_zero
added theorem Nonneg.mk_mul_mk
added theorem Nonneg.mk_nat_cast
added theorem Nonneg.mk_pow
added theorem Nonneg.mk_sub_mk
added theorem Nonneg.nsmul_coe
added theorem Nonneg.nsmul_mk
added def Nonneg.toNonneg
added theorem Nonneg.toNonneg_coe
added theorem Nonneg.toNonneg_le
added theorem Nonneg.toNonneg_lt