expOrderIso — Mathlib

English

The exponential map establishes an order isomorphism between the additive group G and the unit group of WithZero on G, i.e., exp: G → Gᵐ⁰ˣ is an order-preserving bijection with a two-sided inverse given by log.

Русский

Экспоненциальная карта порождает упорядоченное изоморфизм между аддитивной группой G и группой единиц WithZero на G: отображение exp: G → Gᵐ⁰ˣ является обеим инъекцией/биекция с сохранением порядка, имея обратное отображение log.

LaTeX

$$$\exp: G \to G^{\times}_{0}$ является упорядоченным изоморфизмом.$$

Lean4

/-- The exponential map as an order isomorphism between `G` and `Gᵐ⁰ˣ`. -/
@[simps!]
def expOrderIso : G ≃o Gᵐ⁰ˣ where
  __ := expEquiv
  map_rel_iff' := by simp [← Units.val_le_val]

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