Theorems · Theorem · group theory
sub_eq_self
∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, a - b = a ↔ b = 0- Defined in
- Mathlib.Algebra.Group.Basic
- Cited by
- 11 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.
Cites4
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
- sub_eq_add_negproof · cited by 1,023
- neg_eq_zeroproof · cited by 171
- add_eq_leftproof · cited by 37
Cited by11
Results whose statement or proof uses this declaration.
- BumpCovering.toPOUFun_eq_mul_prodproof · cited by 3
- FractionalIdeal.count_coeproof · cited by 1
- extDerivWithin_apply_vectorField_of_pairwise_commuteproof · cited by 1
- Nat.count_modEq_card_eq_ceilproof · cited by 1
- ZMod.completedLFunction_one_sub_evenproof · cited by 1
- LightCondensed.internallyProjective_free_natUnionInftyproof · cited by 0
- factorPowSucc.isUnit_of_isUnit_imageproof · cited by 0
- Polynomial.isFixedPt_newtonMap_of_isUnit_iffproof · cited by 0
- LinearRecurrence.charPoly_monicproof · cited by 0
- Matrix.add_mul_mul_mul_invOf_eq_one'proof · cited by 0
- ArithmeticFunction.sum_moebius_mul_log_eqproof · cited by 0