Documentation

Mathlib.Algebra.Order.Monoid.Defs

Ordered monoids #

This file provides the definitions of ordered monoids.

class OrderedAddCommMonoid (α : Type u_2) extends AddCommMonoid α, PartialOrder α :
Type u_2

An ordered (additive) commutative monoid is a commutative monoid with a partial order such that addition is monotone.

Instances
class OrderedCommMonoid (α : Type u_2) extends CommMonoid α, PartialOrder α :
Type u_2

An ordered commutative monoid is a commutative monoid with a partial order such that multiplication is monotone.

Instances
class OrderedCancelAddCommMonoid (α : Type u_2) extends OrderedAddCommMonoid α :
Type u_2

An ordered cancellative additive commutative monoid is a partially ordered commutative additive monoid in which addition is cancellative and monotone.

Instances
class OrderedCancelCommMonoid (α : Type u_2) extends OrderedCommMonoid α :
Type u_2

An ordered cancellative commutative monoid is a partially ordered commutative monoid in which multiplication is cancellative and monotone.

Instances

A linearly ordered additive commutative monoid.

Instances
class LinearOrderedCommMonoid (α : Type u_2) extends OrderedCommMonoid α, LinearOrder α :
Type u_2

A linearly ordered commutative monoid.

Instances

A linearly ordered cancellative additive commutative monoid is an additive commutative monoid with a decidable linear order in which addition is cancellative and monotone.

Instances

A linearly ordered cancellative commutative monoid is a commutative monoid with a linear order in which multiplication is cancellative and monotone.

Instances
@[simp]
theorem one_le_mul_self_iff {α : Type u_1} [LinearOrderedCommMonoid α] {a : α} :
1 a * a 1 a
@[simp]
theorem nonneg_add_self_iff {α : Type u_1} [LinearOrderedAddCommMonoid α] {a : α} :
0 a + a 0 a
@[simp]
theorem one_lt_mul_self_iff {α : Type u_1} [LinearOrderedCommMonoid α] {a : α} :
1 < a * a 1 < a
@[simp]
theorem pos_add_self_iff {α : Type u_1} [LinearOrderedAddCommMonoid α] {a : α} :
0 < a + a 0 < a
@[simp]
theorem mul_self_le_one_iff {α : Type u_1} [LinearOrderedCommMonoid α] {a : α} :
a * a 1 a 1
@[simp]
theorem add_self_nonpos_iff {α : Type u_1} [LinearOrderedAddCommMonoid α] {a : α} :
a + a 0 a 0
@[simp]
theorem mul_self_lt_one_iff {α : Type u_1} [LinearOrderedCommMonoid α] {a : α} :
a * a < 1 a < 1
@[simp]
theorem add_self_neg_iff {α : Type u_1} [LinearOrderedAddCommMonoid α] {a : α} :
a + a < 0 a < 0