Theorems · Theorem · group theory
eq_sub_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
- 65 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
- sub_eq_add_negproof · cited by 1,023
- eq_add_neg_iff_add_eqproof · cited by 12
Cited by65
Results whose statement or proof uses this declaration.
- Polynomial.modByMonic_add_divproof · cited by 25
- eq_sub_iff_add_eq'proof · cited by 21
- RootPairing.InvariantForm.two_mul_apply_root_rootproof · cited by 10
- PowerSeries.IsWeierstrassDivisorAt.eq_of_mul_add_eq_mul_addproof · cited by 7
- Finset.sum_erase_eq_subproof · cited by 6
- Real.sin_sqproof · cited by 6
- integral_sin_powproof · cited by 5
- Int.fract_eq_iffproof · cited by 4
- Polynomial.self_sub_monomial_natDegree_leadingCoeffproof · cited by 4
- Submodule.projection_eq_self_sub_projectionproof · cited by 4
- LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iffproof · cited by 3
- EuclideanGeometry.mul_dist_eq_abs_sub_sq_distproof · cited by 3