Unit subgroups of a ring

def Units.posSubgroup (R : Type u_1) [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] : Subgroup Rˣ

The subgroup of positive units of a linear ordered semiring.

Equations

• Units.posSubgroup R = { carrier := {x : Rˣ | 0 < ↑x}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[simp]

theorem Units.mem_posSubgroup {R : Type u_1} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] (u : Rˣ) : u ∈ posSubgroup R ↔ 0 < ↑u