The submonoid of positive elements

@[simp]

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

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.mem_pos {α : Type u_1} [MulZeroOneClass α] [PartialOrder α] [PosMulStrictMono α] [ZeroLEOneClass α] [NeZero 1] {a : α} : a ∈ Submonoid.pos α ↔ 0 < a