The submonoid of positive elements

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

The submonoid of positive elements.

Equations

• Submonoid.pos α = { carrier := Set.Ioi 0, mul_mem' := ⋯, one_mem' := ⋯ }

@[simp]

theorem Submonoid.coe_pos (α : Type u_1) [MulZeroOneClass α] [PartialOrder α] [PosMulStrictMono α] [ZeroLEOneClass α] [NeZero 1] : ↑(pos α) = Set.Ioi 0

@[simp]

theorem Submonoid.mem_pos {α : Type u_1} [MulZeroOneClass α] [PartialOrder α] [PosMulStrictMono α] [ZeroLEOneClass α] [NeZero 1] {a : α} : a ∈ pos α ↔ 0 < a