toMulRightReflectLT

Mathlib.Algebra.Order.Monoid.Defs

URI: https://scilib.ai/kg/mathlib#IsOrderedCancelMonoid.toMulRightReflectLT

English

Right multiplication preserves strict order: if a < b, then a c < b c.

Русский

Правое умножение сохраняет строгое неравенство: если a < b, то a c < b c.

LaTeX

$$a < b \Rightarrow a c < b c$$

Lean4

@[to_additive]
theorem toMulRightReflectLT : MulRightReflectLT α :=
  inferInstance

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

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

Разделы

Аффилиация

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