Theorems · Theorem · group theory
neg_sub_neg
∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b : α), -a - -b = b - a- Defined in
- Mathlib.Algebra.Group.Basic
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses propext
- Assumes
- SubtractionCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- add_commproof · cited by 1,535
- sub_eq_add_negproof · cited by 1,023
- neg_negproof · cited by 960
- SubtractionCommMonoidstatement and proof · cited by 79
Cited by13
Results whose statement or proof uses this declaration.
- slope_negproof · cited by 10
- RootPairing.InvariantForm.two_mul_apply_root_rootproof · cited by 10
- abs_min_sub_min_le_maxproof · cited by 4
- MeasureTheory.Measure.addHaar_submoduleproof · cited by 3
- ConvexCone.IsReproducing.of_span_eq_topproof · cited by 2
- Real.smul_map_volume_mul_leftproof · cited by 2
- lp.hasSum_singleproof · cited by 2
- NonemptyInterval.length_negproof · cited by 2
- trapezoidal_error_symmproof · cited by 1
- ZetaAsymptotics.term_oneproof · cited by 1
- MeasureTheory.supermartingale_of_condExp_sub_nonneg_natproof · cited by 0
- Rat.uniformContinuous_negproof · cited by 0