Basic facts for unbundled linear ordered (semi)fields

@[simp]

theorem inv_pos {α : Type u_1} [Semifield α] [LinearOrder α] [PosMulReflectLT α] [ZeroLEOneClass α] {a : α} : 0 < a⁻¹ ↔ 0 < a

theorem inv_pos_of_pos {α : Type u_1} [Semifield α] [LinearOrder α] [PosMulReflectLT α] [ZeroLEOneClass α] {a : α} : 0 < a → 0 < a⁻¹

Alias of the reverse direction of inv_pos.

@[simp]

theorem inv_nonneg {α : Type u_1} [Semifield α] [LinearOrder α] [PosMulReflectLT α] [ZeroLEOneClass α] {a : α} : 0 ≤ a⁻¹ ↔ 0 ≤ a

theorem inv_nonneg_of_nonneg {α : Type u_1} [Semifield α] [LinearOrder α] [PosMulReflectLT α] [ZeroLEOneClass α] {a : α} : 0 ≤ a → 0 ≤ a⁻¹

Alias of the reverse direction of inv_nonneg.

@[simp]

theorem inv_lt_zero {α : Type u_1} [Semifield α] [LinearOrder α] [PosMulReflectLT α] [ZeroLEOneClass α] {a : α} : a⁻¹ < 0 ↔ a < 0

@[simp]

theorem inv_nonpos {α : Type u_1} [Semifield α] [LinearOrder α] [PosMulReflectLT α] [ZeroLEOneClass α] {a : α} : a⁻¹ ≤ 0 ↔ a ≤ 0

theorem one_div_pos {α : Type u_1} [Semifield α] [LinearOrder α] [PosMulReflectLT α] [ZeroLEOneClass α] {a : α} : 0 < 1 / a ↔ 0 < a

theorem one_div_neg {α : Type u_1} [Semifield α] [LinearOrder α] [PosMulReflectLT α] [ZeroLEOneClass α] {a : α} : 1 / a < 0 ↔ a < 0

theorem one_div_nonneg {α : Type u_1} [Semifield α] [LinearOrder α] [PosMulReflectLT α] [ZeroLEOneClass α] {a : α} : 0 ≤ 1 / a ↔ 0 ≤ a

theorem one_div_nonpos {α : Type u_1} [Semifield α] [LinearOrder α] [PosMulReflectLT α] [ZeroLEOneClass α] {a : α} : 1 / a ≤ 0 ↔ a ≤ 0

theorem div_pos {α : Type u_1} [Semifield α] [LinearOrder α] [PosMulReflectLT α] [ZeroLEOneClass α] {a : α} {b : α} [PosMulStrictMono α] (ha : 0 < a) (hb : 0 < b) : 0 < a / b

theorem div_nonneg {α : Type u_1} [Semifield α] [LinearOrder α] [PosMulReflectLT α] [ZeroLEOneClass α] {a : α} {b : α} [PosMulMono α] (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a / b

theorem div_nonpos_of_nonpos_of_nonneg {α : Type u_1} [Semifield α] [LinearOrder α] [PosMulReflectLT α] [ZeroLEOneClass α] {a : α} {b : α} [MulPosMono α] (ha : a ≤ 0) (hb : 0 ≤ b) : a / b ≤ 0

theorem div_nonpos_of_nonneg_of_nonpos {α : Type u_1} [Semifield α] [LinearOrder α] [PosMulReflectLT α] [ZeroLEOneClass α] {a : α} {b : α} [PosMulMono α] (ha : 0 ≤ a) (hb : b ≤ 0) : a / b ≤ 0

theorem zpow_nonneg {α : Type u_1} [Semifield α] [LinearOrder α] [PosMulReflectLT α] [ZeroLEOneClass α] {a : α} [PosMulMono α] (ha : 0 ≤ a) (n : ℤ) : 0 ≤ a ^ n

theorem zpow_pos_of_pos {α : Type u_1} [Semifield α] [LinearOrder α] [PosMulReflectLT α] [ZeroLEOneClass α] {a : α} [PosMulStrictMono α] (ha : 0 < a) (n : ℤ) : 0 < a ^ n