hahnEmbedding_isOrderedAddMonoid

1000+ list: Hahn embedding theorem

∀ (M : Type u_1) [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  ∃ f,
    Function.Injective ⇑f ∧
      ∀ (a : M), ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso M) (ofLex (f a)).orderTop

Hahn embedding theorem For a linearly ordered additive group M, there exists an injective OrderAddMonoidHom from M to Lex ℝ⟦FiniteArchimedeanClass M⟧ that sends each a : M to an element of the a-Archimedean class of the Hahn series.

Defined in: Mathlib.RingTheory.HahnSeries.HahnEmbedding
Cited by: 0 results in Mathlib
Foundations: Depth 164 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddCommGroup LinearOrder IsOrderedAddMonoid

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites49

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Realstatement and proof · cited by 25,697
RingHom.idproof · cited by 18,349
AddCommGroupstatement and proof · cited by 12,871
LinearMapproof · cited by 10,215
Top.topstatement and proof · cited by 9,680
LinearOrderstatement and proof · cited by 8,572
Equivstatement · cited by 8,337
WithTopstatement · cited by 3,754
IsOrderedAddMonoidstatement and proof · cited by 1,659
WithTop.someproof · cited by 1,128
OrderIsostatement · cited by 874

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.