unitsCongr — Mathlib

English

An isomorphism of ordered monoids descends to their units.

Русский

Изоморфизм упорядоченных моноидов порождает изоморфизм их единиц.

LaTeX

$$$ \text{unitsCongr}: \alpha^{\times} \simeq_o \beta^{\times} $$$

Lean4

/-- An isomorphism of ordered monoids descends to their units. -/
@[simps!]
def unitsCongr {α β : Type*} [Preorder α] [Monoid α] [Preorder β] [Monoid β] (e : α ≃*o β) : αˣ ≃*o βˣ
    where
  __ := Units.mapEquiv e.toMulEquiv
  map_le_map_iff' {x y} := by simp [← Units.val_le_val]

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