Mathlib v3 is deprecated. Go to Mathlib v4

Theorem one_le_mul_of_one_le_of_one_le

Modification history

2022-10-08 09:14
src/algebra/order/ring.lean
feat(algebra/order/ring): Non-cancellative ordered semirings (#16172) …
Modified one_le_mul_of_one_le_of_one_leView on Github →
2021-05-07 09:30
src/algebra/ordered_ring.lean
refactor(*): more choice-free proofs (#7455) …
Modified one_le_mul_of_one_le_of_one_leView on Github →
2021-02-11 16:20
src/algebra/ordered_ring.lean
feat(algebra/ordered_ring): a product is at least one if both factors are (#6172) …
Added one_le_mul_of_one_le_of_one_leView on Github →
2020-07-03 22:00
src/algebra/ordered_group.lean
chore(algebra/ordered_group): deduplicate (#3279) …
Deleted one_le_mul_of_one_le_of_one_leView on Github →
2020-07-01 07:55
src/algebra/ordered_group.lean
feat(ring_theory/valuation): definition and basic properties of valuations (#3222) …
Added one_le_mul_of_one_le_of_one_leView on Github →