Commit 2021-02-11 16:20 b9354dda

feat(algebra/ordered_ring): a product is at least one if both factors are (#6172) Add single lemma one_le_mul_of_one_le_of_one_le The lemma is stated for an ordered_semiring, but only multiplication is used. There does not seem to be an ordered_monoid class where this lemma would fit. Relevant Zulip chat: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/ordered_monoid.3F