Theorems · Theorem · group theory
sub_add_cancel_right
∀ {G : Type u_3} [inst : AddGroup G] (a b : G), a - (b + a) = -b- Defined in
- Mathlib.Algebra.Group.Basic
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 12 from the axioms · uses propext
- Assumes
- AddGroup
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.
- AddGroupstatement and proof · cited by 4,410
- neg_subproof · cited by 272
- add_sub_cancel_rightproof · cited by 187
Cited by17
Results whose statement or proof uses this declaration.
- RootPairing.root_sub_root_mem_of_pairingIn_posproof · cited by 7
- intervalIntegral.intervalIntegrable_log'proof · cited by 2
- Complex.GammaSeq_tendsto_Gammaproof · cited by 2
- Int.fib_add_twoproof · cited by 2
- Set.image_sub_leftproof · cited by 2
- RootPairing.Base.forall_mem_support_invtSubmodule_iffproof · cited by 1
- Nat.frequently_modEqproof · cited by 1
- EReal.sub_add_cancel_rightproof · cited by 1
- AddCommGroup.zsmul_add_modEqproof · cited by 1
- CochainComplex.mappingCone.δ_sndproof · cited by 1
- HurwitzZeta.cosZeta_one_subproof · cited by 1
- Module.involutive_preReflectionproof · cited by 1