Commit 2024-07-15 23:26 71254516

View on Github →

chore (Algebra.Order.Nonneg.Ring): split into unbundled and bundled ordered ring files (#14370) We split Algebra.Order.Nonneg.Ring into Algebra.Order.Ring.Unbundled.Nonneg which uses unbundled ordered algebra typeclasses, eg CovariantClass, and Algebra.Order.Nonneg.Ring which uses bundled class, eg OrderedAddComm. Using this we can avoid importing bundled ordered algebra classes until later downstream.

Estimated changes

deleted theorem Nonneg.bot_eq
deleted def Nonneg.coeRingHom
deleted theorem Nonneg.coe_toNonneg
deleted theorem Nonneg.mk_add_mk
deleted theorem Nonneg.mk_eq_one
deleted theorem Nonneg.mk_eq_zero
deleted theorem Nonneg.mk_mul_mk
deleted theorem Nonneg.mk_natCast
deleted theorem Nonneg.mk_pow
deleted theorem Nonneg.mk_sub_mk
deleted theorem Nonneg.nsmul_coe
deleted theorem Nonneg.nsmul_mk
deleted def Nonneg.toNonneg
deleted theorem Nonneg.toNonneg_coe
deleted theorem Nonneg.toNonneg_le
deleted theorem Nonneg.toNonneg_lt
deleted theorem Nonneg.toNonneg_of_nonneg
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_natCast
added theorem Nonneg.mk_pow
added theorem Nonneg.mk_sub_mk
added theorem Nonneg.nsmul_coe
added theorem Nonneg.nsmul_mk
added theorem Nonneg.pow_nonneg
added def Nonneg.toNonneg
added theorem Nonneg.toNonneg_coe
added theorem Nonneg.toNonneg_le
added theorem Nonneg.toNonneg_lt