Documentation

Mathlib.Algebra.Ring.Subring.Units

Unit subgroups of a ring #

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
    @[simp]
    theorem Units.mem_posSubgroup {R : Type u_1} [LinearOrderedSemiring R] (u : Rˣ) :