toPosMulReflectLT

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs

URI: https://scilib.ai/kg/mathlib#MulLeftMono.toPosMulReflectLT

English

From left-multiplicative monotonicity, derive a PosMulReflectLT structure.

Русский

Из монотонности слева по умножению следует структура PosMulReflectLT.

LaTeX

$$MulLeftMono α ⇒ PosMulReflectLT α$$

Lean4

instance (priority := 100) toPosMulReflectLT [MulLeftReflectLT α] : PosMulReflectLT α where
  elim _ _ := ‹MulLeftReflectLT α›.elim _

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

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

Разделы

Аффилиация

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