Theorems · Inductive type · group theory
IsCancelMul
(G : Type u) → [Mul G] → Prop
A mixin for cancellative multiplication.
- Defined in
- Mathlib.Algebra.Group.Defs
- Cited by
- 32 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- Mul
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by37
Results whose statement or proof uses this declaration.
- ThreeGPFree.smul_setstatement and proof · cited by 2
- Function.Injective.isCancelMulstatement and proof · cited by 2
- Set.MulAntidiagonal.fst_eq_fst_iff_snd_eq_sndstatement and proof · cited by 2
- Set.MulAntidiagonal.finite_of_isPWOstatement and proof · cited by 1
- threeGPFree_insertstatement and proof · cited by 1
- threeGPFree_smul_setstatement and proof · cited by 1
- Set.MulAntidiagonal.eq_of_fst_le_fst_of_snd_le_sndstatement and proof · cited by 1
- Commute.of_orderOf_dvd_twostatement and proof · cited by 1
- mul_comm_of_exponent_twostatement and proof · cited by 1
- mulLeftEmbedding_eq_mulRightEmbeddingstatement and proof · cited by 1
- isCancelMul_iffstatement and proof · cited by 1
- isCancelMul_iff_forall_isRegularstatement · cited by 1