Isomorphism of ordered monoids descends to units

def OrderMonoidIso.unitsCongr {α : Type u_1} {β : Type u_2} [Preorder α] [Monoid α] [Preorder β] [Monoid β] (e : α ≃*o β) : αˣ ≃*o βˣ

An isomorphism of ordered monoids descends to their units.

Equations

• e.unitsCongr = { toMulEquiv := Units.mapEquiv e.toMulEquiv, map_le_map_iff' := ⋯ }

@[simp]

theorem OrderMonoidIso.val_unitsCongr_apply {α : Type u_1} {β : Type u_2} [Preorder α] [Monoid α] [Preorder β] [Monoid β] (e : α ≃*o β) (a✝ : αˣ) : ↑(e.unitsCongr a✝) = e ↑a✝

@[simp]

theorem OrderMonoidIso.val_unitsCongr_symm_apply {α : Type u_1} {β : Type u_2} [Preorder α] [Monoid α] [Preorder β] [Monoid β] (e : α ≃*o β) (a : βˣ) : ↑(e.unitsCongr.symm a) = (↑e).symm ↑a

@[simp]

theorem OrderMonoidIso.val_inv_unitsCongr_apply {α : Type u_1} {β : Type u_2} [Preorder α] [Monoid α] [Preorder β] [Monoid β] (e : α ≃*o β) (a✝ : αˣ) : ↑(e.unitsCongr a✝)⁻¹ = e ↑a✝⁻¹

@[simp]

theorem OrderMonoidIso.val_inv_unitsCongr_symm_apply {α : Type u_1} {β : Type u_2} [Preorder α] [Monoid α] [Preorder β] [Monoid β] (e : α ≃*o β) (a : βˣ) : ↑(e.unitsCongr.symm a)⁻¹ = (↑e).symm ↑a⁻¹

theorem OrderMonoidIso.unitsCongr_symm_apply {α : Type u_1} {β : Type u_2} [Preorder α] [Monoid α] [Preorder β] [Monoid β] (e : α ≃*o β) (x : βˣ) : ↑(e.unitsCongr.symm x) = e.symm ↑x