mulLeft — Mathlib

English

x ↦ a · x defines an order isomorphism α ≃o α when α is a group with a compatible order.

Русский

x ↦ a · x задает порядок-изоморфизм.

LaTeX

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

Lean4

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

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