toPosMulReflectLE

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs

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

English

From left-strict-monotonicity, deduce a PosMulReflectLE structure.

Русский

Из свойства слева строгой монотонности следует PosMulReflectLE.

LaTeX

$$MulLeftStrictMono α ⇒ PosMulReflectLE α$$

Lean4

instance (priority := 100) toPosMulReflectLE [MulLeftReflectLE α] : PosMulReflectLE α where
  elim _ _ := ‹MulLeftReflectLE α›.elim _

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

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

Разделы

Аффилиация

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