Theorems · Theorem · group theory
sub_eq_neg_add
∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b : α), a - b = -b + a- Defined in
- Mathlib.Algebra.Group.Basic
- Cited by
- 51 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.
Cites3
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
- SubtractionCommMonoidstatement and proof · cited by 79
Cited by51
Results whose statement or proof uses this declaration.
- add_sub_cancel_leftproof · cited by 198
- dist_eq_norm_subproof · cited by 29
- Function.Periodic.sub_eq'proof · cited by 9
- Real.Angle.angle_eq_iff_two_pi_dvd_subproof · cited by 8
- Function.Periodic.nat_mul_sub_eqproof · cited by 6
- LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeffproof · cited by 6
- Function.Antiperiodic.sub_eq'proof · cited by 5
- Finset.affineCombinationLineMapWeights_apply_leftproof · cited by 5
- dist_eq_norm_sub'proof · cited by 4
- LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iffproof · cited by 3
- LaurentSeries.valuation_le_iff_coeff_lt_eq_zeroproof · cited by 3
- Complex.arg_conjproof · cited by 3