The submonoid of positive elements #
def
Submonoid.pos
(α : Type u_1)
[MulZeroOneClass α]
[PartialOrder α]
[PosMulStrictMono α]
[ZeroLEOneClass α]
[NeZero 1]
:
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]
:
↑(Submonoid.pos α) = Set.Ioi 0
@[simp]
theorem
Submonoid.mem_pos
{α : Type u_1}
[MulZeroOneClass α]
[PartialOrder α]
[PosMulStrictMono α]
[ZeroLEOneClass α]
[NeZero 1]
{a : α}
:
a ∈ Submonoid.pos α ↔ 0 < a