mathlib3
6df15017 - feat(algebra/ordered_ring): weaken hypotheses for one_le_two (#6034)

Commit

5 years ago

feat(algebra/ordered_ring): weaken hypotheses for one_le_two (#6034) Adjust `one_le_two` to not require nontriviality.

Author

b-mehta

Parents