Theorems · Theorem · order theory
tsub_add_eq_add_tsub
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
[inst_4 : Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α], b ≤ a → a - b + c = a + c - b- Cited by
- 23 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
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
- AddLeftMonostatement and proof · cited by 687
- ExistsAddOfLEstatement and proof · cited by 330
- OrderedSubstatement and proof · cited by 236
- AddCommSemigroupstatement and proof · cited by 178
- AddLeftReflectLEstatement and proof · cited by 119
- Contravariant.AddLECancellableproof · cited by 45
- AddLECancellable.tsub_add_eq_add_tsubproof · cited by 2
Cited by23
Results whose statement or proof uses this declaration.
- Polynomial.coeff_mirrorproof · cited by 4
- Subgroup.is_ascending_rev_series_of_is_descendingproof · cited by 3
- Subgroup.is_descending_rev_series_of_is_ascendingproof · cited by 3
- MonomialOrder.sPolynomial_monomial_mulproof · cited by 3
- Finset.sum_antidiagonal_choose_succ_nsmulproof · cited by 3
- Finpartition.equitabilise_auxproof · cited by 3
- sum_range_powproof · cited by 2
- AddSubgroup.is_ascending_rev_series_of_is_descendingproof · cited by 2
- AddSubgroup.is_descending_rev_series_of_is_ascendingproof · cited by 2
- lucas_primalityproof · cited by 2
- Finset.local_lubell_yamamoto_meshalkin_inequality_divproof · cited by 2
- NNReal.sqrt_mul_lt_half_add_of_neproof · cited by 1