Theorems · Theorem · group theory
eq_add_neg_iff_add_eq
∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, a = b + -c ↔ a + c = b- Defined in
- Mathlib.Algebra.Group.Basic
- Cited by
- 12 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_add_cancel_rightproof · cited by 75
- add_neg_cancel_rightproof · cited by 65
Cited by12
Results whose statement or proof uses this declaration.
- eq_sub_iff_add_eqproof · cited by 65
- QuotientAddGroup.leftRel_applyproof · cited by 20
- AddSemiconjBy.neg_symm_left_iffproof · cited by 3
- Finset.sum_Ico_eq_add_negproof · cited by 2
- Finset.card_vadd_inter_vaddproof · cited by 2
- ProfiniteGrp.closedAddSubgroup_eq_sInf_openproof · cited by 0
- AddGroupExtension.Section.exists_add_eq_add_add_inlproof · cited by 0
- AddGroupExtension.Section.exists_add_eq_inl_add_addproof · cited by 0
- AddMonoidAlgebra.coeff_mul_apply_rightproof · cited by 0
- AddMonoidAlgebra.coeff_mul_single_applyproof · cited by 0
- QuotientAddGroup.rightRel_eq_topproof · cited by 0
- add_zsmul_addproof · cited by 0