toMulLeftMono

Mathlib.Algebra.Order.Ring.Canonical

URI: https://scilib.ai/kg/mathlib#CanonicallyOrderedAdd.toMulLeftMono

← MathLib Explorer

English

If a ≤ b, then a·c ≤ b·c for all c.

Русский

Если a ≤ b, то a·c ≤ b·c для всякого c.

LaTeX

$$$a \le b \Rightarrow a c \le b c$$$

Lean4

instance (priority := 100) toMulLeftMono [NonUnitalNonAssocSemiring R] [LE R] [CanonicallyOrderedAdd R] :
    MulLeftMono R := by
  refine ⟨fun a b c h => ?_⟩
  dsimp
  rcases exists_add_of_le h with ⟨c, rfl⟩
  rw [mul_add]
  apply self_le_add_right

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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