Documentation

Mathlib.RingTheory.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
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Units.mem_posSubgroup {R : Type u_1} [LinearOrderedSemiring R] (u : Rˣ) :
    u ∈ Units.posSubgroup R ↔ 0 < ↑u