nonunitsOrderEmbedding — Mathlib

English

The map A ↦ A.nonunits is an order-embedding into the dual order on Subsemigroup K.

Русский

Отображение A ↦ A.nonunits является вложением по порядку в двойственный порядок на Subsemigroup K.

LaTeX

$$$\text{nonunitsOrderEmbedding}:\ ValuationSubring K \hookrightarrow_{\mathrm{ord}} (\operatorname{Subsemigroup} K)^{\mathrm{op}}$$$

Lean4

/-- The map on valuation subrings to their nonunits is a dual order embedding. -/
def nonunitsOrderEmbedding : ValuationSubring K ↪o (Subsemigroup K)ᵒᵈ
    where
  toFun A := A.nonunits
  inj' := nonunits_injective
  map_rel_iff' {_A _B} := nonunits_le_nonunits

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