Theorems · Theorem · group theory
sub_eq_sub_iff_add_eq_add
∀ {G : Type u_3} [inst : AddCommGroup G] {a b c d : G}, a - b = c - d ↔ a + d = c + b- Defined in
- Mathlib.Algebra.Group.Basic
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses propext
- Assumes
- AddCommGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddCommGroupstatement and proof · cited by 12,871
- add_commproof · cited by 1,535
- sub_eq_iff_eq_addproof · cited by 74
- sub_eq_iff_eq_add'proof · cited by 33
- sub_add_eq_add_subproof · cited by 29
Cited by9
Results whose statement or proof uses this declaration.
- AddCommGroup.modEq_iff_zsmulproof · cited by 5
- FractionalIdeal.count_well_definedproof · cited by 5
- Polynomial.natDegree_sub_eq_of_prod_eqproof · cited by 3
- MeasureTheory.martingalePart_add_ae_eqproof · cited by 1
- roth_3ap_theoremproof · cited by 1
- groupCohomology.smul_map_inv_sub_map_inv_of_isCocycle₂proof · cited by 0
- add_neg_eq_add_neg_iff_add_eq_addproof · cited by 0
- groupCohomology.cocycles₂_ρ_map_inv_sub_map_invproof · cited by 0
- neg_add_eq_neg_add_iff_add_eq_addproof · cited by 0