Documentation

Init.Grind.Ordered.Field

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) :
a b * c⁻¹ a * c b
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) :
a < b * c⁻¹ a * c < b
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) :
a * b⁻¹ < c a < c * 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) :
a b * c⁻¹ b a * c
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) :
a * b⁻¹ c c * b a
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) :
a < b * c⁻¹ b < a * c
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) :
a * b⁻¹ < c c * b < a
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) :
a * c < b * c a < b
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) :
c * a < c * b a < b
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) :
a * c < b * c b < a
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) :
c * a < c * b b < a
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) :
a * c b * c a b
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) :
c * a c * b a b
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) :
a * c b * c b a
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) :
c * a c * b b a