Theorems · Theorem · group theory
sub_sub_cancel
∀ {G : Type u_3} [inst : AddCommGroup G] (a b : G), a - (a - b) = b- Defined in
- Mathlib.Algebra.Group.Basic
- Cited by
- 105 results in Mathlib
- Foundations
- Depth 14 from the axioms, rests on 62 definitions · uses propext
- Assumes
- AddCommGroup
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.
- AddCommGroupstatement and proof · cited by 12,871
- sub_sub_selfproof · cited by 12
Cited by105
Results whose statement or proof uses this declaration.
- unitInterval.symm_symmproof · cited by 7
- Algebra.Generators.Cotangent.exactproof · cited by 6
- Int.fract_eq_iffproof · cited by 4
- Real.binEntropy_one_subproof · cited by 4
- self_sub_toIcoModproof · cited by 3
- self_sub_toIocModproof · cited by 3
- analyticAt_inverseproof · cited by 3
- PhragmenLindelof.horizontal_stripproof · cited by 3
- LinearMap.IsIdempotentElem.ker_eq_rangeproof · cited by 3
- Affine.Simplex.sSameSide_affineSpan_faceOpposite_of_sign_eqproof · cited by 3
- AffineIndependent.affineCombination_mem_shift_iffproof · cited by 3
- MeasureTheory.convolutionExistsAt_flipproof · cited by 3