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

theorem RingHom.isUnit_eqLocusS_mk_iff {R : Type u_1} {T : Type u_2} [Semiring T] [Semiring R] (f g : R →+* T) {r : R} (hr : f r = g r) : IsUnit ⟨r, hr⟩ ↔ IsUnit r

theorem RingHom.isUnit_eqLocus_mk_iff {R : Type u_1} {T : Type u_2} [Semiring T] [Ring R] (f g : R →+* T) {r : R} (hr : f r = g r) : IsUnit ⟨r, hr⟩ ↔ IsUnit r

instance RingHom.instIsLocalHomSubtypeMemSubsemiringEqLocusSSubtype {R : Type u_1} {T : Type u_2} [Semiring T] [Semiring R] (f g : R →+* T) : IsLocalHom (f.eqLocusS g).subtype

instance RingHom.instIsLocalHomSubtypeMemSubringEqLocusSubtype {R : Type u_1} {T : Type u_2} [Semiring T] [Ring R] (f g : R →+* T) : IsLocalHom (f.eqLocus g).subtype