mulRight — Mathlib

English

In a linearly ordered monoid, the map x ↦ x·m is an order-embedding: it preserves the order strictly, i.e., x < y implies x·m < y·m.

Русский

В линейно упорядоченном моноиде отображение x ↦ x·m является вложением по порядку: оно строго монотонно сохраняет порядок, т.е. x < y ⇒ x·m < y·m.

LaTeX

$$$\forall x,y \in \alpha\ (x

Lean4

/-- The order embedding sending `b` to `b * a`, for some fixed `a`.
See also `OrderIso.mulRight` when working in an ordered group. -/
@[to_additive (attr := simps!) /-- The order embedding sending `b` to `b + a`, for some fixed `a`.
           See also `OrderIso.addRight` when working in an additive ordered group. -/
    ]
def mulRight {α : Type*} [Mul α] [LinearOrder α] [MulRightStrictMono α] (m : α) : α ↪o α :=
  OrderEmbedding.ofStrictMono (fun n => n * m) fun _ _ w => mul_lt_mul_right' w m

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