Hahn Integer Part Refinement Criterion Proof #
theorem
ConwayRefinement.Standalone.Hahn.HahnIntegerPartRefinementCriterion.proof
{G : Type u}
{R : Type v}
[AddCommGroup G]
[LinearOrder G]
[IsOrderedAddMonoid G]
[Module ℚ G]
[IsOrderedModule ℚ G]
[Field R]
:
Conditions (A1)--(A3) and the common-tail conditions imply four-factor refinement.