Documentation

Mathlib.Algebra.Order.GroupWithZero.Submonoid

The submonoid of positive elements #

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

The submonoid of positive elements.

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