English
There is an order isomorphism between a group and its order dual induced by left scalar multiplication by a negative scalar; this maps elements to their dual order consistently with the order.
Русский
Существуют отображение-порядок-изоморфизм между группой и её двойственным порядком, индуцируемое левой умножением на отрицательный скаляр; оно сохраняет порядок в согласованности с двойственным порядком.
LaTeX
$$$ smulRightDual(ha) : G \cong_o G^{\mathrm{op}} $ where \ ha: a<0$$
Lean4
/-- Left scalar multiplication as an order isomorphism. -/
@[simps!]
def smulRightDual (ha : a < 0) : G ≃o Gᵒᵈ
where
toEquiv := (Equiv.smulRight ha.ne).trans toDual
map_rel_iff' := (@OrderDual.toDual_le_toDual G).trans <| smul_le_smul_iff_of_neg_left ha
