Finite index of the positive-units subgroup

For a linearly ordered ring, the positive units Units.posSubgroup R form an index-2 subgroup, so it has finite index. Together with the general finite-index-preimage instance (Subgroup.instFiniteIndexComap), this yields the finiteness of the totally positive units of a number field, hence of its narrow class group.

instance Units.instFiniteIndexPosSubgroup (R : Type u_1) [Ring R] [LinearOrder R] [IsStrictOrderedRing R] : (posSubgroup R).FiniteIndex

The positive units of a linearly ordered ring form an index-2, hence finite-index, subgroup.