# Documentation

Mathlib.Algebra.Order.Field.Canonical.Defs

# Canonically ordered semifields #

class CanonicallyLinearOrderedSemifield (α : Type u_2) extends , , , , , , :
Type u_2
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : αα
• nsmul_zero : ∀ (x : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = x +
• add_comm : ∀ (a b : α), a + b = b + a
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• add_le_add_left : ∀ (a b : α), a b∀ (c : α), c + a c + b
• bot : α
• bot_le : ∀ (x : α), x
• exists_add_of_le : ∀ {a b : α}, a bc, b = a + c
• le_self_add : ∀ (a b : α), a a + b
• mul : ααα
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• natCast : α
• natCast_zero :
• natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) =
• npow : αα
• npow_zero : ∀ (x : α),
• npow_succ : ∀ (n : ) (x : α),
• mul_comm : ∀ (a b : α), a * b = b * a
• eq_zero_or_eq_zero_of_mul_eq_zero : ∀ {a b : α}, a * b = 0a = 0 b = 0
• le_of_add_le_add_left : ∀ (a b c : α), a + b a + cb c

Additive cancellation is compatible with the order in an ordered cancellative additive commutative monoid.

• exists_pair_ne : x y, x y
• zero_le_one : 0 1

In a strict ordered semiring, 0 ≤ 1.

• mul_lt_mul_of_pos_left : ∀ (a b c : α), a < b0 < cc * a < c * b

Left multiplication by a positive element is strictly monotone.

• mul_lt_mul_of_pos_right : ∀ (a b c : α), a < b0 < ca * c < b * c

Right multiplication by a positive element is strictly monotone.

• min : ααα
• max : ααα
• compare : ααOrdering
• le_total : ∀ (a b : α), a b b a

A linear order is total.

• decidableLE : DecidableRel fun x x_1 => x x_1

In a linearly ordered type, we assume the order relations are all decidable.

• decidableEq :

In a linearly ordered type, we assume the order relations are all decidable.

• decidableLT : DecidableRel fun x x_1 => x < x_1

In a linearly ordered type, we assume the order relations are all decidable.

• min_def : ∀ (a b : α), min a b = if a b then a else b

The minimum function is equivalent to the one you get from minOfLe.

• max_def : ∀ (a b : α), max a b = if a b then b else a

The minimum function is equivalent to the one you get from maxOfLe.

• compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b =

Comparison via compare is equal to the canonical comparison given decidable < and =.

• inv : αα
• div : ααα
• div_eq_mul_inv : ∀ (a b : α), a / b = a * b⁻¹

a / b := a * b⁻¹

• zpow : αα

The power operation: a ^ n = a * ··· * a; a ^ (-n) = a⁻¹ * ··· a⁻¹ (n times)

• zpow_zero' : ∀ (a : α),

a ^ 0 = 1

• zpow_succ' : ∀ (n : ) (a : α),

a ^ (n + 1) = a * a ^ n

• zpow_neg' : ∀ (n : ) (a : α),

a ^ -(n + 1) = (a ^ (n + 1))⁻¹

• inv_zero : 0⁻¹ = 0

The inverse of 0 in a group with zero is 0.

• mul_inv_cancel : ∀ (a : α), a 0a * a⁻¹ = 1

Every nonzero element of a group with zero is invertible.

A canonically linear ordered field is a linear ordered field in which a ≤ b iff there exists c with b = a + c.

Instances