English
There is an order embedding from Units α into α given by val; i.e., val is an order-embedding with inj, and preserves order.
Русский
Существует порядок-встраивание из Units α в α, заданное отображением val; т.е. val является порядковым вложением с инъективностью и сохраняет порядок.
LaTeX
$$$\\mathrm{orderEmbeddingVal}: \\mathrm{Units}(\\alpha) \\hookrightarrow_{\\text{order}} \\alpha \\,\\text{с map} = \\mathrm{val}, \\ \\, \\mathrm{inj}=\\mathrm{val\\_injective}$$$
Lean4
/-- `val : αˣ → α` as an order embedding. -/
@[to_additive (attr := simps -fullyApplied) /-- `val : add_units α → α` as an order embedding. -/
]
def orderEmbeddingVal [Monoid α] [LinearOrder α] : αˣ ↪o α :=
⟨⟨val, val_injective⟩, .rfl⟩
