Theorems · Theorem · group theory
neg_eq_iff_add_eq_zero
∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, -a = b ↔ a + b = 0- Defined in
- Mathlib.Algebra.Group.Basic
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext
- Assumes
- AddGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
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
- add_eq_zero_iff_neg_eqproof · cited by 11
Cited by16
Results whose statement or proof uses this declaration.
- Complex.conj_eq_iff_improof · cited by 9
- Ring.neg_one_ne_one_of_char_ne_twoproof · cited by 5
- CharTwo.neg_eqproof · cited by 4
- DihedralGroup.not_commutativeproof · cited by 2
- aleph0_le_rank_of_isEmpty_oreSetproof · cited by 1
- Matrix.submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_detproof · cited by 1
- ZMod.neg_eq_self_iffproof · cited by 1
- CategoryTheory.IsPushout.mono_of_isPullback_of_monoproof · cited by 1
- Ring.eq_self_iff_eq_zero_of_char_ne_twoproof · cited by 1
- IsPreconnected.eq_of_sq_eqproof · cited by 1
- Equiv.pointReflection_fixed_iff_of_injective_two_nsmulproof · cited by 1
- Equiv.injective_pointReflection_left_of_injective_two_nsmulproof · cited by 1