Theorems · Definition · order theory

HahnSeries.embDomainOrderAddMonoidHom

{Γ : Type u_1} →
  {R : Type u_2} →
    [inst : LinearOrder Γ] →
      [inst_1 : PartialOrder R] →
        {Γ' : Type u_3} →
          [inst_2 : LinearOrder Γ'] → Γ ↪o Γ' → [inst_3 : AddMonoid R] → Lex (HahnSeries Γ R) →+o Lex (HahnSeries Γ' R)

HahnSeries.embDomain as an OrderAddMonoidHom.

Defined in

Mathlib.RingTheory.HahnSeries.Lex

Cited by

3 results in Mathlib

Foundations

Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LinearOrderPartialOrderLinearOrderAddMonoid