embDomainRingHom_C — Mathlib

English

There exists a ring homomorphism embDomainRingHom that extends an order-embedding to a Hahn-series domain, preserving ring operations.

Русский

Существует кольцевой однозначный морфизм embDomainRingHom, который расширяет отображение порядка до области HahnSeries и сохраняет операции кольца.

LaTeX

$$embDomainRingHom f hfi hf : HahnSeries Γ R →+* HahnSeries Γ' R$$

Lean4

theorem embDomainRingHom_C [NonAssocSemiring R] {f : Γ →+ Γ'} {hfi : Function.Injective f}
    {hf : ∀ g g' : Γ, f g ≤ f g' ↔ g ≤ g'} {r : R} : embDomainRingHom f hfi hf (C r) = C r :=
  embDomain_single.trans (by simp)

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