Theorems · Theorem · order theory
tsub_tsub
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] (b a c : α),
b - a - c = b - (a + c)- Defined in
- Mathlib.Algebra.Order.Sub.Defs
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PartialOrderstatement and proof · cited by 6,410
- le_antisymmproof · cited by 2,068
- le_reflproof · cited by 2,061
- add_assocproof · cited by 746
- OrderedSubstatement and proof · cited by 236
- AddCommSemigroupstatement and proof · cited by 178
- tsub_le_iff_leftproof · cited by 38
Cited by9
Results whose statement or proof uses this declaration.
- tsub_add_eq_tsub_tsubproof · cited by 7
- tsub_add_tsub_cancelproof · cited by 5
- coeff_minpolyDiv_sub_pow_mem_spanproof · cited by 1
- Finset.le_card_falling_div_chooseproof · cited by 1
- Stirling.log_stirlingSeq_formulaproof · cited by 1
- NNReal.sqrt_mul_lt_half_add_of_neproof · cited by 1
- trapezoidal_integral_symmproof · cited by 1
- AddLECancellable.tsub_add_tsub_commproof · cited by 1
- tsub_tsub_tsub_cancel_rightproof · cited by 0