mulRight — Mathlib

English

x ↦ x · a defines an order-isomorphism α ≃o α for a group α with order structure.

Русский

x ↦ x · a задает биективное отображение сохраняющее порядок.

LaTeX

$$OrderIso.mulRight(a) : α ≃o α$$

Lean4

/-- `Equiv.mulRight` as an `OrderIso`. See also `OrderEmbedding.mulRight`. -/
@[to_additive (attr := simps! +simpRhs toEquiv apply) /--
    `Equiv.addRight` as an `OrderIso`. See also `OrderEmbedding.addRight`. -/
    ]
def mulRight (a : α) : α ≃o α where
  map_rel_iff' {_ _} := mul_le_mul_iff_right a
  toEquiv := Equiv.mulRight a

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