smulRight — Mathlib

English

For a > 0, the map b ↦ b • a is an order isomorphism of β, with inverse given by b ↦ b • a⁻¹.

Русский

При a > 0 отображение b ↦ b • a является порядковым изоморфизмом β, обратное задаётся как b ↦ b • a⁻¹.

LaTeX

$$$\\forall a>0,\\; f(b)=b\\cdot a\\; :\\; \\beta \\to \\beta \\text{ is an order isomorphism with inverse } g(b)=b\\cdot a^{-1}$$$

Lean4

/-- Right scalar multiplication as an order isomorphism. -/
@[simps!]
def smulRight [PosSMulMono α β] [PosSMulReflectLE α β] {a : α} (ha : 0 < a) : β ≃o β
    where
  toEquiv := Equiv.smulRight ha.ne'
  map_rel_iff' := smul_le_smul_iff_of_pos_left ha

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