of_mul_lt_mul_left — Mathlib

English

If left-multiplication preserves strict order, then the structure is an ordered cancellative monoid.

Русский

Если левое умножение сохраняет строгость порядка, то структура образует упорядоченный моноид с отменой.

LaTeX

$$ (\forall a,b,c, b < c \Rightarrow a*b < a*c) \Rightarrow IsOrderedCancelMonoid α$$

Lean4

@[to_additive]
theorem of_mul_lt_mul_left {α : Type*} [CommMonoid α] [LinearOrder α] (hmul : ∀ a b c : α, b < c → a * b < a * c) :
    IsOrderedCancelMonoid α
    where
  mul_le_mul_left a b h
    c := by
    obtain rfl | h := eq_or_lt_of_le h
    · simp
    exact (hmul _ _ _ h).le
  le_of_mul_le_mul_left a b c
    h := by
    contrapose! h
    exact hmul _ _ _ h

Похожие утверждения