toMulPosStrictMono

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs

URI: https://scilib.ai/kg/mathlib#MulRightStrictMono.toMulPosStrictMono

English

If a ≥ 0 and b·a < c·a, then b < c.

Русский

Пусть a ≥ 0 и b·a < c·a. Тогда b < c.

LaTeX

$$$[MulPosReflectLT α] \ (a \ge 0) \land (b a < c a) \Rightarrow b < c$$$

Lean4

instance (priority := 100) toMulPosStrictMono [MulRightStrictMono α] : MulPosStrictMono α where
  elim _ _ := ‹MulRightStrictMono α›.elim _

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

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

Разделы

Аффилиация

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