Theorems · Theorem · order theory

HahnSeries.embDomainOrderEmbedding_apply

∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : PartialOrder R] {Γ' : Type u_3}
  [inst_2 : LinearOrder Γ'] (f : Γ ↪o Γ') [inst_3 : Zero R] (a : Lex (HahnSeries Γ R)),
  (HahnSeries.embDomainOrderEmbedding f) a = toLex (HahnSeries.embDomain f (ofLex a))

Defined in

Mathlib.RingTheory.HahnSeries.Lex

Cited by

1 results in Mathlib

Foundations

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

Assumes

LinearOrderPartialOrderLinearOrderZero