Mathlib Map

Theorems · Theorem · order theory

cmp_add_right

∀ {α : Type u_3} [inst : Add α] [inst_1 : LinearOrder α] [AddRightStrictMono α] (a b c : α),
  cmp (a + c) (b + c) = cmp a b
Defined in
Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Cited by
2 results in Mathlib
Foundations
Depth 20 from the axioms · uses propext
Assumes
AddLinearOrderAddRightStrictMono
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

UpperHalfPlane.cmp_dist_eq_cmp_dist_coe_center · cited by 5UpperHalfPlane.cmp_dist_e…cmp_sub_zero · cited by 1cmp_sub_zeroLinearOrder · cited by 8572LinearOrderAddRightStrictMono · cited by 160AddRightStrictMonocmp · cited by 43cmpstrictMono_id · cited by 16strictMono_idStrictMono.cmp_map_eq · cited by 7StrictMono.cmp_map_eqStrictMono.add_const · cited by 6StrictMono.add_constcmp_add_rightCITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.