Theorems · Theorem · group theory
sub_add_cancel_left
∀ {G : Type u_3} [inst : AddCommGroup G] (a b : G), a - (a + b) = -b- Defined in
- Mathlib.Algebra.Group.Basic
- Cited by
- 19 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
- neg_subproof · cited by 272
- add_sub_cancel_leftproof · cited by 198
Cited by19
Results whose statement or proof uses this declaration.
- Nat.add_modEq_left_iffproof · cited by 4
- RootPairing.pairing_reflectionPerm_self_rightproof · cited by 4
- HasSum.hasSum_symmetricIco_of_hasSum_symmetricIccproof · cited by 3
- Complex.Gamma_mul_Gamma_one_subproof · cited by 3
- RootPairing.pairing_reflectionPerm_self_leftproof · cited by 3
- Real.strictAnti_eulerMascheroniSeq'proof · cited by 2
- Module.Dual.eq_of_preReflection_mapsToproof · cited by 2
- Int.add_modEq_left_iffproof · cited by 2
- PowerSeries.IsWeierstrassDivisorAt.coeff_seq_memproof · cited by 2
- ArchimedeanClass.mk_left_le_mk_add_iffproof · cited by 2
- tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_supportproof · cited by 1