Theorems · Theorem · group theory
neg_add_eq_zero
∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, -a + b = 0 ↔ a = b- Defined in
- Mathlib.Algebra.Group.Basic
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 13 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_injproof · cited by 85
- add_eq_zero_iff_eq_negproof · cited by 49
Cited by14
Results whose statement or proof uses this declaration.
- AddMonoidHom.ker_eq_bot_iffproof · cited by 14
- MeasureTheory.Measure.pairwise_aedisjoint_of_aedisjoint_forall_ne_zeroproof · cited by 2
- cauchy_davenport_minOrder_addproof · cited by 2
- isCancelVAdd_iff_eq_zero_of_vadd_eqproof · cited by 2
- IsAddQuotientCoveringMap.isCancelVAddproof · cited by 1
- crossProduct_ne_zero_iff_linearIndependentproof · cited by 1
- tendsto_norm_neg_add_self_nhdsNEproof · cited by 1
- AddSubgroup.add_injective_of_disjointproof · cited by 0
- MeasureTheory.IsAddFundamentalDomain.exists_ne_zero_vadd_eqproof · cited by 0
- UniqueSums.toTwoUniqueSums_of_addGroupproof · cited by 0
- NonarchimedeanAddGroup.exists_openAddSubgroup_separatingproof · cited by 0