embDomainOrderAddMonoidHom — Mathlib

English

The embedding lifts to an order-preserving monoid homomorphism between Lex(HahnSeries Γ R) and Lex(HahnSeries Γ' R).

Русский

Вложение порождает моноидогомоморфизм, сохраняющий порядок, между Lex(HahnSeries Γ R) и Lex(HahnSeries Γ' R).

LaTeX

$$$\mathrm{embDomainOrderAddMonoidHom}(f) : \mathrm{Lex}(\ HahnSeries Γ R) \rightarrow_+^o \mathrm{Lex}(\ HahnSeries Γ' R)$$$

Lean4

/-- `HahnSeries.embDomain` as an `OrderAddMonoidHom`. -/
@[simps]
noncomputable def embDomainOrderAddMonoidHom [AddMonoid R] : Lex (HahnSeries Γ R) →+o Lex (HahnSeries Γ' R)
    where
  __ := (embDomainOrderEmbedding f).toOrderHom
  map_zero' := by simp
  map_add' := by simp [embDomainOrderEmbedding, embDomain_add]

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