Canonically ordered semifields

ink

class CanonicallyLinearOrderedSemifield (α : Type u_1) extends CanonicallyOrderedCommSemiring , Nontrivial , Min , Max , Inv , Div : 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 : DecidableEq α

• 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 (Int.ofNat (Nat.succ n)) a = a * zpow (Int.ofNat n) a) _auto✝

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

  zpow_neg' : autoParam (∀ (n : ℕ) (a : α), zpow (Int.negSucc n) a = (zpow (↑(Nat.succ n)) 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 ≠ 0 → a * 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.

ink

instance CanonicallyLinearOrderedSemifield.toLinearOrderedCommGroupWithZero {α : Type u_1} [inst : CanonicallyLinearOrderedSemifield α] : LinearOrderedCommGroupWithZero α

Equations

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

ink

instance CanonicallyLinearOrderedSemifield.toCanonicallyLinearOrderedAddMonoid {α : Type u_1} [inst : CanonicallyLinearOrderedSemifield α] : CanonicallyLinearOrderedAddMonoid α

Equations

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