# Documentation

Mathlib.Algebra.Order.Field.Canonical.Defs

# Canonically ordered semifields #

class CanonicallyLinearOrderedSemifield (α : Type u_1) extends , , , , , :
Type u_1
• toMin : Min α
• toMax : Max α
• A linear order is total.

le_total : ∀ (a b : α), a b b a
• In a linearly ordered type, we assume the order relations are all decidable.

decidable_le : DecidableRel fun x x_1 => x x_1
• In a linearly ordered type, we assume the order relations are all decidable.

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

decidable_lt : DecidableRel fun x x_1 => x < x_1
• The minimum function is equivalent to the one you get from minOfLe.

min_def : autoParam (∀ (a b : α), min a b = if a b then a else b) _auto✝
• The minimum function is equivalent to the one you get from maxOfLe.

max_def : autoParam (∀ (a b : α), max a b = if a b then b else a) _auto✝
• toInv : Inv α
• toDiv : Div α
• a / b := a * b⁻¹⁻¹

div_eq_mul_inv : autoParam (∀ (a b : α), a / b = a * b⁻¹) _auto✝
• The power operation: a ^ n = a * ··· * a; a ^ (-n) = a⁻¹ * ··· a⁻¹⁻¹ * ··· a⁻¹⁻¹ (n times)

zpow : αα
• a ^ 0 = 1

zpow_zero' : autoParam (∀ (a : α), zpow 0 a = 1) _auto✝
• a ^ (n + 1) = a * a ^ n

zpow_succ' : autoParam (∀ (n : ) (a : α), zpow () a = a * zpow () a) _auto✝
• a ^ -(n + 1) = (a ^ (n + 1))⁻¹⁻¹

zpow_neg' : autoParam (∀ (n : ) (a : α), zpow () a = (zpow (↑()) a)⁻¹) _auto✝
• The inverse of 0 in a group with zero is 0.

inv_zero : 0⁻¹ = 0
• Every nonzero element of a group with zero is invertible.

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

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

Instances
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.