toMulRightMono

Mathlib.Algebra.Order.Ring.Canonical

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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