toPosSMulStrictMono

Mathlib.Algebra.Order.Module.Defs

URI: https://scilib.ai/kg/mathlib#PosSMulReflectLE.toPosSMulStrictMono

← MathLib Explorer

English

An instance provides IsOrderedModule α α from IsOrderedRing α.

Русский

Экземпляр предоставляет IsOrderedModule α α из IsOrderedRing α.

LaTeX

$$$IsOrderedRing\;\alpha \Rightarrow IsOrderedModule\;\alpha\;\alpha$$$

Lean4

theorem toPosSMulStrictMono [PosSMulReflectLE α β] : PosSMulStrictMono α β where
  smul_lt_smul_of_pos_left _a ha _b₁ _b₂ hb := not_le.1 fun h ↦ hb.not_ge <| le_of_smul_le_smul_left h ha

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

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

Разделы

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

Аффилиация

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