Theorems · Theorem · order theory

HahnEmbedding.Seed.coeff_baseEmbedding

∀ {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) {x : ↥seed.baseEmbedding.domain}
  {f : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c)},
  (↑x = f.sum fun c => ⇑(seed.stratum c).subtype) →
    ∀ (c : FiniteArchimedeanClass M), (ofLex (↑seed.baseEmbedding x)).coeff c = (seed.coeff c) (f c)

Defined in

Mathlib.Algebra.Order.Module.HahnEmbedding

Cited by

3 results in Mathlib

Foundations

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

Assumes

DivisionRingLinearOrderIsOrderedRingArchimedeanAddCommGroupLinearOrderIsOrderedAddMonoidModuleIsOrderedModuleAddCommGroupLinearOrderModule