Theorems · Theorem · order theory
add_tsub_cancel_left
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α]
[AddLeftReflectLE α] (a b : α), a + b - a = b- Defined in
- Mathlib.Algebra.Order.Sub.Defs
- Cited by
- 42 results in Mathlib
- Foundations
- Depth 12 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- OrderedSubstatement and proof · cited by 236
- AddCommSemigroupstatement and proof · cited by 178
- AddLeftReflectLEstatement and proof · cited by 119
- Contravariant.AddLECancellableproof · cited by 45
- AddLECancellable.add_tsub_cancel_leftproof · cited by 3
Cited by42
Results whose statement or proof uses this declaration.
- Nat.card_unitsproof · cited by 6
- Polynomial.natDegree_divByMonicproof · cited by 5
- MvPowerSeries.coeff_add_monomial_mulproof · cited by 4
- Submodule.eq_factor_of_eq_factor_succproof · cited by 4
- Polynomial.coeff_mirrorproof · cited by 4
- Nat.binomial_eq_chooseproof · cited by 3
- Multiset.revzip_powersetAux_lemmaproof · cited by 3
- Polynomial.homogenize_monomialproof · cited by 3
- cauchySeq_of_edist_le_of_summableproof · cited by 2
- Polynomial.bernoulli_comp_neg_Xproof · cited by 2
- Polynomial.coeff_homogenizeproof · cited by 2
- Finset.HasAntidiagonal.filter_fst_eq_antidiagonalproof · cited by 2