Theorems · Theorem · group theory
add_right_cancel
∀ {G : Type u_1} [inst : Add G] [IsRightCancelAdd G] {a b c : G}, a + b = c + b → a = c- Defined in
- Mathlib.Algebra.Group.Defs
- Cited by
- 23 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- Assumes
- AddIsRightCancelAdd
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.
- IsRightCancelAddstatement and proof · cited by 69
- IsRightCancelAdd.add_right_cancelproof · cited by 1
Cited by23
Results whose statement or proof uses this declaration.
- add_left_injectiveproof · cited by 49
- add_right_cancel_iffproof · cited by 19
- AddCommGroup.ModEq.add_iff_leftproof · cited by 3
- HahnSeries.coeff_mul_single_addproof · cited by 3
- Function.Injective.isRightCancelAddproof · cited by 3
- AddSubgroup.isComplement_univ_singletonproof · cited by 3
- Topology.IsQuotientMap.isAddQuotientCoveringMap_of_addSubgroupproof · cited by 3
- Set.AddAntidiagonal.fst_eq_fst_iff_snd_eq_sndproof · cited by 2
- threeAPFree_insertproof · cited by 1
- AddSubgroup.isComplement_singleton_rightproof · cited by 1
- AddCommMagma.IsRightCancelAdd.toIsLeftCancelAddproof · cited by 1
- Equiv.Perm.cycleType_mul_inv_mem_cycleFactorsFinset_eq_subproof · cited by 1