Theorems · Theorem · group theory
IsCancelSMul.right_cancel
∀ {G : Type u_11} {P : Type u_12} [inst : SMul G P] [IsCancelSMul G P] (a b : G) (c : P), a • c = b • c → a = b- Defined in
- Mathlib.Algebra.Group.Action.Defs
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
- Assumes
- SMulIsCancelSMul
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.
- IsCancelSMulstatement and proof · cited by 14
- IsCancelSMul.right_cancel'proof · cited by 2
Cited by5
Results whose statement or proof uses this declaration.
- IsCancelSMul.eq_one_of_smulproof · cited by 2
- IsQuotientCoveringMap.toPermFiber_extproof · cited by 1
- IsQuotientCoveringMap.fundamentalGroupToMulOpposite_eq_one_iffproof · cited by 1
- Set.SMulAntidiagonal.fst_eq_fst_iff_snd_eq_sndproof · cited by 1
- isQuotientCoveringMap_iff_isCoveringMap_andproof · cited by 0