Theorems · Theorem · group theory
add_sub_sub_cancel
∀ {G : Type u_3} [inst : AddCommGroup G] (a b c : G), a + b - (a - c) = b + c- Defined in
- Mathlib.Algebra.Group.Basic
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext
- Assumes
- AddCommGroup
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.
- AddCommGroupstatement and proof · cited by 12,871
- add_sub_cancel_leftproof · cited by 198
- sub_addproof · cited by 51
Cited by14
Results whose statement or proof uses this declaration.
- Complex.cosh_sub_sinhproof · cited by 4
- PhragmenLindelof.horizontal_stripproof · cited by 3
- ProbabilityTheory.integrable_rpow_mul_exp_of_integrable_exp_mulproof · cited by 3
- Metric.diam_sphere_eqproof · cited by 2
- ProbabilityTheory.integrable_exp_mul_abs_addproof · cited by 2
- ProbabilityTheory.integrable_rpow_abs_mul_exp_add_of_integrable_exp_mulproof · cited by 2
- abs_sub_eq_two_nsmul_negPartproof · cited by 1
- stereo_right_invproof · cited by 1
- Real.singleton_eq_inter_Iccproof · cited by 1
- RCLike.sub_conjproof · cited by 0
- CFC.abs_sub_selfproof · cited by 0
- Int.fract_eq_fractproof · cited by 0