unitGroupOrderEmbedding — Mathlib

English

The map A ↦ A.unitGroup is an order embedding from ValuationSubring K into the order of subgroups of K×.

Русский

Отображение A ↦ A.unitGroup является вложением по порядку из множества valuation-подкольц в порядок подгрупп K×.

LaTeX

$$$\text{unitGroupOrderEmbedding}:\ Emph{ValuationSubring }K \hookrightarrow_{\mathrm{ord}} (\operatorname{Subgroup} K^{\times})$$$

Lean4

/-- The map on valuation subrings to their unit groups is an order embedding. -/
def unitGroupOrderEmbedding : ValuationSubring K ↪o Subgroup Kˣ
    where
  toFun A := A.unitGroup
  inj' := unitGroup_injective
  map_rel_iff' {_A _B} := unitGroup_le_unitGroup

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