Theorems · Inductive type · order theory

HahnEmbedding.Seed

(K : Type u_1) →
  [inst : DivisionRing K] →
    [inst_1 : LinearOrder K] →
      [IsOrderedRing K] →
        [Archimedean K] →
          (M : Type u_2) →
            [inst_4 : AddCommGroup M] →
              [inst_5 : LinearOrder M] →
                [IsOrderedAddMonoid M] →
                  [inst_7 : Module K M] →
                    [IsOrderedModule K M] →
                      (R : Type u_3) → [inst_9 : AddCommGroup R] → [LinearOrder R] → [Module K R] → Type (max u_2 u_3)

HahnEmbedding.Seed extends HahnEmbedding.ArchimedeanStrata by specifying strictly monotone linear maps from each stratum to module R.

Defined in

Mathlib.Algebra.Order.Module.HahnEmbedding

Cited by

55 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Quot.sound

Assumes

DivisionRingLinearOrderIsOrderedRingArchimedeanAddCommGroupLinearOrderIsOrderedAddMonoidModuleIsOrderedModuleAddCommGroupLinearOrderModule