Documentation

Mathlib.Algebra.Order.Field.Defs

Linear ordered (semi)fields #

A linear ordered (semi)field is a (semi)field equipped with a linear order such that

Main Definitions #

A linear ordered semifield is a field with a linear order respecting the operations.

  • add : ααα
  • 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 : α), AddMonoid.nsmul 0 x = 0
  • nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
  • add_comm : ∀ (a b : α), a + b = b + a
  • 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.natCast 0 = 0
  • natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
  • npow : αα
  • npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
  • npow_succ : ∀ (n : ) (x : α), Semiring.npow (n + 1) x = Semiring.npow n x * x
  • 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
  • le_of_add_le_add_left : ∀ (a b c : α), a + b a + cb c
  • exists_pair_ne : ∃ (x : α), ∃ (y : α), x y
  • zero_le_one : 0 1
  • mul_lt_mul_of_pos_left : ∀ (a b c : α), a < b0 < cc * a < c * b
  • mul_lt_mul_of_pos_right : ∀ (a b c : α), a < b0 < ca * c < b * c
  • mul_comm : ∀ (a b : α), a * b = b * a
  • min : ααα
  • max : ααα
  • compare : ααOrdering
  • le_total : ∀ (a b : α), a b b a
  • decidableLE : DecidableRel fun (x1 x2 : α) => x1 x2
  • decidableEq : DecidableEq α
  • decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2
  • min_def : ∀ (a b : α), min a b = if a b then a else b
  • max_def : ∀ (a b : α), max a b = if a b then b else a
  • compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b = compareOfLessAndEq a b
  • 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 : α), LinearOrderedSemifield.zpow 0 a = 1

    a ^ 0 = 1

  • zpow_succ' : ∀ (n : ) (a : α), LinearOrderedSemifield.zpow (Int.ofNat n.succ) a = LinearOrderedSemifield.zpow (Int.ofNat n) a * a

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

  • zpow_neg' : ∀ (n : ) (a : α), LinearOrderedSemifield.zpow (Int.negSucc n) a = (LinearOrderedSemifield.zpow (↑n.succ) 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.

  • nnratCast : ℚ≥0α
  • nnratCast_def : ∀ (q : ℚ≥0), q = q.num / q.den

    However NNRat.cast is defined, it must be propositionally equal to a / b.

    Do not use this lemma directly. Use NNRat.cast_def instead.

  • nnqsmul : ℚ≥0αα

    Scalar multiplication by a nonnegative rational number.

    Unless there is a risk of a Module ℚ≥0 _ instance diamond, write nnqsmul := _. This will set nnqsmul to (NNRat.cast · * ·) thanks to unification in the default proof of nnqsmul_def.

    Do not use directly. Instead use the notation.

  • nnqsmul_def : ∀ (q : ℚ≥0) (a : α), LinearOrderedSemifield.nnqsmul q a = q * a

    However qsmul is defined, it must be propositionally equal to multiplication by Rat.cast.

    Do not use this lemma directly. Use NNRat.smul_def instead.

Instances

    A linear ordered field is a field with a linear order respecting the operations.

    • add : ααα
    • 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 : α), AddMonoid.nsmul 0 x = 0
    • nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
    • add_comm : ∀ (a b : α), a + b = b + a
    • 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.natCast 0 = 0
    • natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
    • npow : αα
    • npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
    • npow_succ : ∀ (n : ) (x : α), Semiring.npow (n + 1) x = Semiring.npow n x * x
    • neg : αα
    • sub : ααα
    • sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
    • zsmul : αα
    • zsmul_zero' : ∀ (a : α), Ring.zsmul 0 a = 0
    • zsmul_succ' : ∀ (n : ) (a : α), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul (Int.ofNat n) a + a
    • zsmul_neg' : ∀ (n : ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
    • neg_add_cancel : ∀ (a : α), -a + a = 0
    • intCast : α
    • intCast_ofNat : ∀ (n : ), IntCast.intCast n = n
    • intCast_negSucc : ∀ (n : ), IntCast.intCast (Int.negSucc n) = -(n + 1)
    • 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
    • exists_pair_ne : ∃ (x : α), ∃ (y : α), x y
    • zero_le_one : 0 1
    • mul_pos : ∀ (a b : α), 0 < a0 < b0 < a * b
    • min : ααα
    • max : ααα
    • compare : ααOrdering
    • le_total : ∀ (a b : α), a b b a
    • decidableLE : DecidableRel fun (x1 x2 : α) => x1 x2
    • decidableEq : DecidableEq α
    • decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2
    • min_def : ∀ (a b : α), min a b = if a b then a else b
    • max_def : ∀ (a b : α), max a b = if a b then b else a
    • compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b = compareOfLessAndEq a b
    • mul_comm : ∀ (a b : α), a * b = b * a
    • 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 : α), LinearOrderedField.zpow 0 a = 1

      a ^ 0 = 1

    • zpow_succ' : ∀ (n : ) (a : α), LinearOrderedField.zpow (Int.ofNat n.succ) a = LinearOrderedField.zpow (Int.ofNat n) a * a

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

    • zpow_neg' : ∀ (n : ) (a : α), LinearOrderedField.zpow (Int.negSucc n) a = (LinearOrderedField.zpow (↑n.succ) a)⁻¹

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

    • nnratCast : ℚ≥0α
    • ratCast : α
    • mul_inv_cancel : ∀ (a : α), a 0a * a⁻¹ = 1

      For a nonzero a, a⁻¹ is a right multiplicative inverse.

    • inv_zero : 0⁻¹ = 0

      The inverse of 0 is 0 by convention.

    • nnratCast_def : ∀ (q : ℚ≥0), q = q.num / q.den

      However NNRat.cast is defined, it must be equal to a / b.

      Do not use this lemma directly. Use NNRat.cast_def instead.

    • nnqsmul : ℚ≥0αα

      Scalar multiplication by a nonnegative rational number.

      Unless there is a risk of a Module ℚ≥0 _ instance diamond, write nnqsmul := _. This will set nnqsmul to (NNRat.cast · * ·) thanks to unification in the default proof of nnqsmul_def.

      Do not use directly. Instead use the notation.

    • nnqsmul_def : ∀ (q : ℚ≥0) (a : α), LinearOrderedField.nnqsmul q a = q * a

      However qsmul is defined, it must be propositionally equal to multiplication by Rat.cast.

      Do not use this lemma directly. Use NNRat.smul_def instead.

    • ratCast_def : ∀ (q : ), q = q.num / q.den

      However Rat.cast q is defined, it must be propositionally equal to q.num / q.den.

      Do not use this lemma directly. Use Rat.cast_def instead.

    • qsmul : αα

      Scalar multiplication by a rational number.

      Unless there is a risk of a Module ℚ _ instance diamond, write qsmul := _. This will set qsmul to (Rat.cast · * ·) thanks to unification in the default proof of qsmul_def.

      Do not use directly. Instead use the notation.

    • qsmul_def : ∀ (a : ) (x : α), LinearOrderedField.qsmul a x = a * x

      However qsmul is defined, it must be propositionally equal to multiplication by Rat.cast.

      Do not use this lemma directly. Use Rat.cast_def instead.

    Instances
      @[instance 100]
      Equations
      • LinearOrderedField.toLinearOrderedSemifield = LinearOrderedSemifield.mk LinearOrderedField.zpow LinearOrderedField.nnqsmul
      theorem mul_inv_le_one {α : Type u_1} [LinearOrderedSemifield α] {a : α} :
      a * a⁻¹ 1

      Equality holds when a ≠ 0. See mul_inv_cancel.

      theorem inv_mul_le_one {α : Type u_1} [LinearOrderedSemifield α] {a : α} :
      a⁻¹ * a 1

      Equality holds when a ≠ 0. See inv_mul_cancel.

      theorem mul_inv_left_le {α : Type u_1} [LinearOrderedSemifield α] {a : α} {b : α} (hb : 0 b) :
      a * (a⁻¹ * b) b

      Equality holds when a ≠ 0. See mul_inv_cancel_left.

      theorem le_mul_inv_left {α : Type u_1} [LinearOrderedSemifield α] {a : α} {b : α} (hb : b 0) :
      b a * (a⁻¹ * b)

      Equality holds when a ≠ 0. See mul_inv_cancel_left.

      theorem inv_mul_left_le {α : Type u_1} [LinearOrderedSemifield α] {a : α} {b : α} (hb : 0 b) :
      a⁻¹ * (a * b) b

      Equality holds when a ≠ 0. See inv_mul_cancel_left.

      theorem le_inv_mul_left {α : Type u_1} [LinearOrderedSemifield α] {a : α} {b : α} (hb : b 0) :
      b a⁻¹ * (a * b)

      Equality holds when a ≠ 0. See inv_mul_cancel_left.

      theorem mul_inv_right_le {α : Type u_1} [LinearOrderedSemifield α] {a : α} {b : α} (ha : 0 a) :
      a * b * b⁻¹ a

      Equality holds when b ≠ 0. See mul_inv_cancel_right.

      theorem le_mul_inv_right {α : Type u_1} [LinearOrderedSemifield α] {a : α} {b : α} (ha : a 0) :
      a a * b * b⁻¹

      Equality holds when b ≠ 0. See mul_inv_cancel_right.

      theorem inv_mul_right_le {α : Type u_1} [LinearOrderedSemifield α] {a : α} {b : α} (ha : 0 a) :
      a * b⁻¹ * b a

      Equality holds when b ≠ 0. See inv_mul_cancel_right.

      theorem le_inv_mul_right {α : Type u_1} [LinearOrderedSemifield α] {a : α} {b : α} (ha : a 0) :
      a a * b⁻¹ * b

      Equality holds when b ≠ 0. See inv_mul_cancel_right.