Commit 2024-07-17 17:39 ba665e36

View on Github →

chore (Algebra.Order.Field.Defs): split off results about unbundled ordered algebra (#14451) We should be able to use these results about unbundled ordered algebra without importing the heavy machinery of the bundled typeclasses.

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
modified theorem Nonneg.inv_mk