Theorems · Theorem · order theory
tsub_add_cancel_of_le
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
[inst_4 : Sub α] [OrderedSub α] {a b : α}, a ≤ b → b - a + a = b- Cited by
- 112 results in Mathlib
- Foundations
- Depth 9 from the axioms, rests on 44 definitions · uses propext, Quot.sound
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
- add_commproof · cited by 1,535
- AddLeftMonostatement and proof · cited by 687
- ExistsAddOfLEstatement and proof · cited by 330
- OrderedSubstatement and proof · cited by 236
- AddCommSemigroupstatement and proof · cited by 178
- add_tsub_cancel_of_leproof · cited by 79
Cited by112
Results whose statement or proof uses this declaration.
- Finset.sum_Ico_eq_sum_rangeproof · cited by 10
- add_le_of_le_tsub_right_of_leproof · cited by 8
- PowerSeries.coeff_X_pow_mul'proof · cited by 7
- Nat.factorization_divproof · cited by 7
- FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_zeroproof · cited by 7
- exists_prime_orderOf_dvd_cardproof · cited by 5
- MvPowerSeries.monomial_mul_monomialproof · cited by 5
- tsub_add_tsub_cancelproof · cited by 5
- Nat.length_digitsproof · cited by 5
- MeasureTheory.Measure.sub_applyproof · cited by 5
- Polynomial.coeff_mul_X_pow'proof · cited by 5
- Polynomial.mirror_natDegreeproof · cited by 4