Documentation

Mathlib.Algebra.Ring.Subring.Units

Unit subgroups of a ring #

source
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 = { carrier := {x : Rˣ | 0 < ↑x}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
Instances For
    source
    @[simp]
    theorem Units.mem_posSubgroup {R : Type u_1} [LinearOrderedSemiring R] (u : Rˣ) :
    u ∈ Units.posSubgroup R ↔ 0 < ↑u