Theorems · Theorem · group theory
sub_sub_cancel_left
∀ {G : Type u_3} [inst : AddCommGroup G] (a b : G), a - b - a = -b- Defined in
- Mathlib.Algebra.Group.Basic
- Cited by
- 28 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext
- Assumes
- AddCommGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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_commproof · cited by 1,535
- sub_eq_add_negproof · cited by 1,023
- add_neg_cancel_leftproof · cited by 76
- add_left_commproof · cited by 76
Cited by28
Results whose statement or proof uses this declaration.
- Complex.Gamma_add_oneproof · cited by 12
- RootPairing.setOfPred_root_add_zsmul_eq_Icc_of_linearIndependentproof · cited by 5
- Polynomial.Chebyshev.U_negproof · cited by 3
- Algebra.exists_aeval_invOf_eq_zero_of_idealMap_adjoin_sup_span_eq_topproof · cited by 3
- toIocMod_sub_selfproof · cited by 3
- ContDiffBump.subproof · cited by 2
- Metric.diam_sphere_eqproof · cited by 2
- toIcoMod_sub_selfproof · cited by 2
- Ideal.iInf_pow_smul_eq_bot_of_le_jacobsonproof · cited by 2
- descPochhammer_nonnegproof · cited by 2
- Submodule.mem_invtSubmodule_reflection_iffproof · cited by 2
- strictConvexOn_rpowproof · cited by 2