Documentation

Mathlib.Algebra.Order.Field.Canonical.Defs

Canonically ordered semifields #

  • 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 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.