MulLECancellable

Mathlib.Algebra.Order.Monoid.Unbundled.Basic

URI: https://scilib.ai/kg/mathlib#Contravariant.MulLECancellable

English

The left-cancellation property holds for all elements a in α: a·b ≤ a·c implies b ≤ c.

Русский

Свойство левой отменяемости выполняется для всех a: a·b ≤ a·c ⇒ b ≤ c.

LaTeX

$$$\forall a,b,c,\; a\cdot b \le a\cdot c \Rightarrow b \le c$$$

Lean4

@[to_additive]
theorem MulLECancellable [Mul α] [LE α] [MulLeftReflectLE α] {a : α} : MulLECancellable a := fun _ _ =>
  le_of_mul_le_mul_left'

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru