posSMulStrictMono_iff_PosSMulReflectLE

Mathlib.Algebra.Order.Module.Defs

URI: https://scilib.ai/kg/mathlib#posSMulStrictMono_iff_PosSMulReflectLE

← MathLib Explorer

English

PosSMulStrictMono α β is equivalent to PosSMulReflectLE α β.

Русский

PosSMulStrictMono α β эквивалентно PosSMulReflectLE α β.

LaTeX

$$$PosSMulStrictMono\;\alpha\;\beta \iff PosSMulReflectLE\;\alpha\;\beta$$$

Lean4

theorem posSMulStrictMono_iff_PosSMulReflectLE : PosSMulStrictMono α β ↔ PosSMulReflectLE α β :=
  ⟨fun _ ↦ inferInstance, fun _ ↦ PosSMulReflectLE.toPosSMulStrictMono⟩

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

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

Разделы

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

Аффилиация

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