Theorems · Theorem · group theory
add_add_sub_cancel
∀ {G : Type u_3} [inst : AddCommGroup G] (a b c : G), a + c + (b - c) = a + b- Defined in
- Mathlib.Algebra.Group.Basic
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 15 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_assocproof · cited by 746
- add_sub_cancelproof · cited by 195
Cited by12
Results whose statement or proof uses this declaration.
- realPart_add_I_smul_imaginaryPartproof · cited by 10
- Complex.cosh_add_sinhproof · cited by 5
- ConvexOn.continuousOn_tfaeproof · cited by 3
- RCLike.add_conjproof · cited by 3
- Ideal.span_pair_add_rightproof · cited by 3
- abs_add_eq_two_nsmul_posPartproof · cited by 1
- norm_sub_le_mul_volume_of_norm_lineDeriv_leproof · cited by 1
- Submodule.reflection_subproof · cited by 1
- BoxIntegral.norm_volume_sub_integral_face_upper_sub_lower_smul_leproof · cited by 1
- StarModule.selfAdjointPart_add_skewAdjointPartproof · cited by 0
- CFC.abs_add_selfproof · cited by 0
- Real.two_mul_cos_mul_cosproof · cited by 0