toMulPosMono

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs

URI: https://scilib.ai/kg/mathlib#MulRightMono.toMulPosMono

English

From right-monotonicity, deduce that right-multiplication is PosMonotone.

Русский

Из правой монотонности следует, что право-умножение является PosMonotone.

LaTeX

$$MulRightMono α ⇒ MulPosMono α$$

Lean4

instance (priority := 100) toMulPosMono [MulRightMono α] : MulPosMono α where elim _ _ := ‹MulRightMono α›.elim _

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

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

Разделы

Аффилиация

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