Linear ordered (semi)fields

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

• addition respects the order: a ≤ b → c + a ≤ c + b;
• multiplication of positives is positive: 0 < a → 0 < b → 0 < a * b;
• 0 < 1.

Main Definitions

• LinearOrderedSemifield: Typeclass for linear order semifields.
• LinearOrderedField: Typeclass for linear ordered fields.

class LinearOrderedSemifield (α : Type u_2) extends LinearOrderedCommSemiring , Semifield , StrictOrderedCommSemiring , LinearOrderedSemiring , StrictOrderedSemiring , CommSemiring , LinearOrderedAddCommMonoid , DivisionSemiring , CommGroupWithZero , Semiring , OrderedCancelAddCommMonoid , CommMonoidWithZero , GroupWithZero , Nontrivial , CommMonoid , NNRatCast , NonUnitalSemiring , NonAssocSemiring , MonoidWithZero , NonUnitalNonAssocSemiring , DivInvMonoid , Monoid , MulZeroOneClass , SemigroupWithZero , AddCommMonoidWithOne , CommSemigroup , Inv , Div , MulOneClass , AddMonoidWithOne , OrderedAddCommMonoid , LinearOrder , AddCommMonoid , Distrib , Semigroup , MulZeroClass , NatCast , PartialOrder , AddMonoid , One , AddCommSemigroup , AddSemigroup , AddZeroClass , CommMagma , Mul , Zero , AddCommMagma , Add , Min , Max , Ord , Preorder , LE , LT : Type u_2

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

class LinearOrderedField (α : Type u_2) extends LinearOrderedCommRing , Field , LinearOrderedRing , CommRing , DivisionRing , CommMonoid , StrictOrderedRing , LinearOrder , Ring , OrderedAddCommGroup , DivInvMonoid , Nontrivial , NNRatCast , RatCast , Semiring , AddCommGroup , AddGroupWithOne , NonUnitalSemiring , NonAssocSemiring , MonoidWithZero , NonUnitalNonAssocSemiring , Monoid , MulZeroOneClass , SemigroupWithZero , AddCommMonoidWithOne , CommSemigroup , Inv , Div , MulOneClass , IntCast , AddMonoidWithOne , PartialOrder , AddGroup , AddCommMonoid , Distrib , Semigroup , MulZeroClass , NatCast , SubNegMonoid , AddMonoid , One , Neg , Sub , AddCommSemigroup , AddSemigroup , AddZeroClass , CommMagma , Mul , Zero , AddCommMagma , Add , Min , Max , Ord , Preorder , LE , LT : Type u_2

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

@[instance 100]

instance LinearOrderedField.toLinearOrderedSemifield {α : Type u_1} [LinearOrderedField α] : LinearOrderedSemifield α

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.

theorem mul_div_mul_left_le {α : Type u_1} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (h : 0 ≤ a / b) : c * a / (c * b) ≤ a / b

Equality holds when c ≠ 0. See mul_div_mul_left.

theorem le_mul_div_mul_left {α : Type u_1} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (h : a / b ≤ 0) : a / b ≤ c * a / (c * b)

Equality holds when c ≠ 0. See mul_div_mul_left.

theorem mul_div_mul_right_le {α : Type u_1} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (h : 0 ≤ a / b) : a * c / (b * c) ≤ a / b

Equality holds when c ≠ 0. See mul_div_mul_right.

theorem le_mul_div_mul_right {α : Type u_1} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (h : a / b ≤ 0) : a / b ≤ a * c / (b * c)

Equality holds when c ≠ 0. See mul_div_mul_right.