Documentation

Init.Grind.Ordered.Module

  • neg_le_iff (a b : M) : -a b -b a
  • add_le_left {a b : M} : a b∀ (c : M), a + c b + c
  • hmul_pos (k : Int) {a : M} : 0 < a → (0 < k 0 < k * a)
  • hmul_nonneg {k : Int} {a : M} : 0 k0 a0 k * a
Instances
    theorem Lean.Grind.IntModule.IsOrdered.add_lt_left {M : Type u} [Preorder M] [IntModule M] [IsOrdered M] {a b : M} (h : a < b) (c : M) :
    a + c < b + c
    theorem Lean.Grind.IntModule.IsOrdered.add_le_right {M : Type u} [Preorder M] [IntModule M] [IsOrdered M] (a : M) {b c : M} (h : b c) :
    a + b a + c
    theorem Lean.Grind.IntModule.IsOrdered.add_lt_right {M : Type u} [Preorder M] [IntModule M] [IsOrdered M] (a : M) {b c : M} (h : b < c) :
    a + b < a + c
    theorem Lean.Grind.IntModule.IsOrdered.hmul_neg {M : Type u} [Preorder M] [IntModule M] [IsOrdered M] (k : Int) {a : M} (h : a < 0) :
    0 < k k * a < 0
    theorem Lean.Grind.IntModule.IsOrdered.hmul_nonpos {M : Type u} [Preorder M] [IntModule M] [IsOrdered M] {k : Int} {a : M} (hk : 0 k) (ha : a 0) :
    k * a 0