theorem
Lean.Grind.Field.IsOrdered.pos_of_inv_pos
{R : Type u}
[Field R]
[LinearOrder R]
[Ring.IsOrdered R]
{a : R}
(h : 0 < a⁻¹)
:
theorem
Lean.Grind.Field.IsOrdered.inv_pos_iff
{R : Type u}
[Field R]
[LinearOrder R]
[Ring.IsOrdered R]
{a : R}
:
theorem
Lean.Grind.Field.IsOrdered.inv_neg_iff
{R : Type u}
[Field R]
[LinearOrder R]
[Ring.IsOrdered R]
{a : R}
:
theorem
Lean.Grind.Field.IsOrdered.inv_nonneg_iff
{R : Type u}
[Field R]
[LinearOrder R]
[Ring.IsOrdered R]
{a : R}
:
theorem
Lean.Grind.Field.IsOrdered.inv_nonpos_iff
{R : Type u}
[Field R]
[LinearOrder R]
[Ring.IsOrdered R]
{a : R}
:
theorem
Lean.Grind.Field.IsOrdered.le_mul_inv_iff_mul_le
{R : Type u}
[Field R]
[LinearOrder R]
[Ring.IsOrdered R]
(a b : R)
{c : R}
(h : 0 < c)
:
theorem
Lean.Grind.Field.IsOrdered.lt_mul_inv_iff_mul_lt
{R : Type u}
[Field R]
[LinearOrder R]
[Ring.IsOrdered R]
(a b : R)
{c : R}
(h : 0 < c)
:
theorem
Lean.Grind.Field.IsOrdered.mul_inv_lt_iff_lt_mul
{R : Type u}
[Field R]
[LinearOrder R]
[Ring.IsOrdered R]
(a c : R)
{b : R}
(h : 0 < b)
:
theorem
Lean.Grind.Field.IsOrdered.le_mul_inv_iff_le_mul_of_neg
{R : Type u}
[Field R]
[LinearOrder R]
[Ring.IsOrdered R]
(a b : R)
{c : R}
(h : c < 0)
:
theorem
Lean.Grind.Field.IsOrdered.mul_inv_le_iff_mul_le_of_neg
{R : Type u}
[Field R]
[LinearOrder R]
[Ring.IsOrdered R]
(a c : R)
{b : R}
(h : b < 0)
:
theorem
Lean.Grind.Field.IsOrdered.lt_mul_inv_iff_lt_mul_of_neg
{R : Type u}
[Field R]
[LinearOrder R]
[Ring.IsOrdered R]
(a b : R)
{c : R}
(h : c < 0)
:
theorem
Lean.Grind.Field.IsOrdered.mul_inv_lt_iff_mul_lt_of_neg
{R : Type u}
[Field R]
[LinearOrder R]
[Ring.IsOrdered R]
(a c : R)
{b : R}
(h : b < 0)
:
theorem
Lean.Grind.Field.IsOrdered.mul_lt_mul_iff_of_pos_right
{R : Type u}
[Field R]
[LinearOrder R]
[Ring.IsOrdered R]
{a b c : R}
(h : 0 < c)
:
theorem
Lean.Grind.Field.IsOrdered.mul_lt_mul_iff_of_pos_left
{R : Type u}
[Field R]
[LinearOrder R]
[Ring.IsOrdered R]
{a b c : R}
(h : 0 < c)
:
theorem
Lean.Grind.Field.IsOrdered.mul_lt_mul_iff_of_neg_right
{R : Type u}
[Field R]
[LinearOrder R]
[Ring.IsOrdered R]
{a b c : R}
(h : c < 0)
:
theorem
Lean.Grind.Field.IsOrdered.mul_lt_mul_iff_of_neg_left
{R : Type u}
[Field R]
[LinearOrder R]
[Ring.IsOrdered R]
{a b c : R}
(h : c < 0)
:
theorem
Lean.Grind.Field.IsOrdered.mul_le_mul_iff_of_pos_right
{R : Type u}
[Field R]
[LinearOrder R]
[Ring.IsOrdered R]
{a b c : R}
(h : 0 < c)
:
theorem
Lean.Grind.Field.IsOrdered.mul_le_mul_iff_of_pos_left
{R : Type u}
[Field R]
[LinearOrder R]
[Ring.IsOrdered R]
{a b c : R}
(h : 0 < c)
:
theorem
Lean.Grind.Field.IsOrdered.mul_le_mul_iff_of_neg_right
{R : Type u}
[Field R]
[LinearOrder R]
[Ring.IsOrdered R]
{a b c : R}
(h : c < 0)
:
theorem
Lean.Grind.Field.IsOrdered.mul_le_mul_iff_of_neg_left
{R : Type u}
[Field R]
[LinearOrder R]
[Ring.IsOrdered R]
{a b c : R}
(h : c < 0)
: