Commit 2024-03-20 09:04 61e0ad2f

View on Github →

chore: Move basic ordered field lemmas (#11503) These lemmas are needed to define the semifield structure on NNRat, hence I am repurposing Algebra.Order.Field.Defs from avoiding a timeout (which I believe was solved long ago) to avoiding to import random stuff in the definition of the semifield structure on NNRat (although this PR doesn't actually reduce imports there, it will be in a later PR). Reduce the diff of #11203

Estimated changes

deleted theorem div_nonneg
deleted theorem div_pos
deleted theorem inv_lt_zero
deleted theorem inv_nonneg
deleted theorem inv_nonpos
deleted theorem inv_pos
deleted theorem one_div_neg
deleted theorem one_div_nonneg
deleted theorem one_div_nonpos
deleted theorem one_div_pos
deleted theorem zpow_nonneg
deleted theorem zpow_pos_of_pos
added theorem div_nonneg
added theorem div_pos
added theorem inv_lt_zero
added theorem inv_nonneg
added theorem inv_nonpos
added theorem inv_pos
added theorem one_div_neg
added theorem one_div_nonneg
added theorem one_div_nonpos
added theorem one_div_pos
added theorem zpow_nonneg
added theorem zpow_pos_of_pos