embDomainRingHom — Mathlib

English

Another specialization of embDomain_mul asserting multiplicativity under a compatible order-embedding of the domain.

Русский

Ещё одно уточнение embDomain_mul, утверждающее мультипликативность при совместимом отображении домена.

LaTeX

$$$ embDomain\ f (x \cdot y) = embDomain\ f x \cdot embDomain\ f y $$$

Lean4

/-- Extending the domain of Hahn series is a ring homomorphism. -/
@[simps]
def embDomainRingHom [NonAssocSemiring R] (f : Γ →+ Γ') (hfi : Function.Injective f)
    (hf : ∀ g g' : Γ, f g ≤ f g' ↔ g ≤ g') : HahnSeries Γ R →+* HahnSeries Γ' R
    where
  toFun := embDomain ⟨⟨f, hfi⟩, hf _ _⟩
  map_one' := embDomain_one _ f.map_zero
  map_mul' := embDomain_mul _ f.map_add
  map_zero' := embDomain_zero
  map_add' := embDomain_add _

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