toPosMulStrictMono

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs

URI: https://scilib.ai/kg/mathlib#MulLeftStrictMono.toPosMulStrictMono

English

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

Русский

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

LaTeX

$$$[PosMulReflectLT] \; (a \ge 0) \land (a b < a c) \Rightarrow b < c$$$

Lean4

instance (priority := 100) toPosMulStrictMono [MulLeftStrictMono α] : PosMulStrictMono α where
  elim _ _ := ‹MulLeftStrictMono α›.elim _

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

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

Разделы

Аффилиация

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