Theorems · Theorem · order theory

AddLECancellable.tsub_right_inj

∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {a b c : α},
  AddLECancellable a → AddLECancellable b → AddLECancellable c → b ≤ a → c ≤ a → (a - b = a - c ↔ b = c)

Defined in

Mathlib.Algebra.Order.Sub.Basic

Cited by

2 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext, Quot.sound

Assumes

AddCommMonoidPartialOrderCanonicallyOrderedAddSubOrderedSub