toSMulPosReflectLT

Mathlib.Algebra.Order.Module.Defs

URI: https://scilib.ai/kg/mathlib#SMulPosReflectLE.toSMulPosReflectLT

Lean4

instance (priority := 100) toSMulPosReflectLT [SMulPosReflectLE α β] : SMulPosReflectLT α β :=
  SMulPosReflectLT.of_pos fun b hb a₁ a₂ h ↦
    (le_of_smul_le_smul_of_pos_right h.le hb).lt_of_ne <| by rintro rfl; simp at h

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

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

Разделы

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

Аффилиация

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