Unit subgroups of a ring

def Units.posSubgroup (R : Type u_1) [LinearOrderedSemiring R] : Subgroup Rˣ

The subgroup of positive units of a linear ordered semiring.

Equations

• Units.posSubgroup R = let __src := Submonoid.comap (Units.coeHom R) (Submonoid.pos R); { carrier := {x : Rˣ | 0 < ↑x}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[simp]

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