Theorem le_of_forall_one_lt_lt_mul'

Modification history

2024-07-16 00:30

Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean

chore (Algebra.Order.Monoid.Canonical.Defs): split off `ExistsAddOfLE` and `ExistsMulOfLE` (#14390) …

Modified le_of_forall_one_lt_lt_mul'View on Github →

2022-12-01 10:59

Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean

feat: port Algebra.Order.Monoid.Canonical.Defs (#778) …

Added le_of_forall_one_lt_lt_mul'View on Github →