Documentation

Mathlib.Algebra.Order.GroupWithZero.Submonoid

The submonoid of positive elements #

source
def Submonoid.pos (α : Type u_1) [MulZeroOneClass α] [PartialOrder α] [PosMulStrictMono α] [ZeroLEOneClass α] [NeZero 1] :
Submonoid α

The submonoid of positive elements.

Equations
    Instances For
      source
      @[simp]
      theorem Submonoid.coe_pos (α : Type u_1) [MulZeroOneClass α] [PartialOrder α] [PosMulStrictMono α] [ZeroLEOneClass α] [NeZero 1] :
      ↑(pos α) = Set.Ioi 0
      source
      @[simp]
      theorem Submonoid.mem_pos {α : Type u_1} [MulZeroOneClass α] [PartialOrder α] [PosMulStrictMono α] [ZeroLEOneClass α] [NeZero 1] {a : α} :
      a ∈ pos α ↔ 0 < a