toPosMulMono

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs

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

English

From the property that left-multiplication is monotone (MulLeftMono), one obtains PosMulMono.

Русский

Из свойства, что левое умножение монотонно (MulLeftMono), следует PosMulMono.

LaTeX

$$MulLeftMono α ⇒ PosMulMono α$$

Lean4

instance (priority := 100) toPosMulMono [MulLeftMono α] : PosMulMono α where elim _ _ := ‹MulLeftMono α›.elim _

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

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

Разделы

Аффилиация

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