Theorems · Theorem · order theory

HahnEmbedding.Partial.truncLT_eval_mem_range_extendFun

∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  [inst_12 : IsOrderedAddMonoid R] [inst_13 : Archimedean R] {x : M} (hx : x ∉ (↑f).domain)
  (c : FiniteArchimedeanClass M),
  toLex ((HahnSeries.truncLTLinearMap K c) (ofLex (f.eval x))) ∈ (f.extendFun hx).toFun.range

Defined in: Mathlib.Algebra.Order.Module.HahnEmbedding
Cited by: 1 results in Mathlib
Foundations: Depth 131 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: DivisionRing LinearOrder IsOrderedRing Archimedean AddCommGroup LinearOrder IsOrderedAddMonoid Module IsOrderedModule AddCommGroup LinearOrder Module IsOrderedAddMonoid Archimedean

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites58

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
Modulestatement and proof · cited by 20,661
RingHom.idstatement and proof · cited by 18,349
AddCommGroupstatement and proof · cited by 12,871
LinearMapstatement · cited by 10,215
Top.topstatement · cited by 9,680
LinearOrderstatement and proof · cited by 8,572
Equivstatement · cited by 8,337
Submodulestatement · cited by 7,192
LT.lt.leproof · cited by 2,189
IsOrderedAddMonoidstatement and proof · cited by 1,659
DivisionRingstatement and proof · cited by 1,062

Cited by1

Results whose statement or proof uses this declaration.

HahnEmbedding.Partial.truncLT_mem_range_extendFunproof · cited by 1