Canonically ordered semifields

class CanonicallyLinearOrderedSemifield (α : Type u_2) extends CanonicallyOrderedCommSemiring , Nontrivial , Min , Max , Ord , Inv , Div , NNRatCast : Type u_2

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

• 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
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
• bot : α
• bot_le : ∀ (a : α), ⊥ ≤ a
• exists_add_of_le : ∀ {a b : α}, a ≤ b → ∃ (c : α), 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.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero : ∀ (x : α), CanonicallyOrderedCommSemiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), CanonicallyOrderedCommSemiring.npow (n + 1) x = CanonicallyOrderedCommSemiring.npow n x * x
• mul_comm : ∀ (a b : α), a * b = b * a
• eq_zero_or_eq_zero_of_mul_eq_zero : ∀ {a b : α}, a * b = 0 → a = 0 ∨ b = 0
• le_of_add_le_add_left : ∀ (a b c : α), a + b ≤ a + c → b ≤ c
• 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 < b → 0 < c → c * a < c * b

  Left multiplication by a positive element is strictly monotone.

• mul_lt_mul_of_pos_right : ∀ (a b c : α), a < b → 0 < c → a * 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 (x1 x2 : α) => x1 ≤ x2

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

• decidableEq : DecidableEq α

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

• decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2

  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 = compareOfLessAndEq 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 : α), CanonicallyLinearOrderedSemifield.zpow 0 a = 1

  a ^ 0 = 1

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

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

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

@[instance 100]

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

Equations

• CanonicallyLinearOrderedSemifield.toLinearOrderedCommGroupWithZero = LinearOrderedCommGroupWithZero.mk ⋯ CanonicallyLinearOrderedSemifield.zpow ⋯ ⋯ ⋯ ⋯ ⋯

@[instance 100]

instance CanonicallyLinearOrderedSemifield.toCanonicallyLinearOrderedAddCommMonoid {α : Type u_1} [CanonicallyLinearOrderedSemifield α] : CanonicallyLinearOrderedAddCommMonoid α

Equations

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