Theorems · Theorem · group theory
nsmul_right_inj
∀ {M : Type u_1} [inst : AddMonoid M] [IsAddTorsionFree M] {n : ℕ} {a b : M}, n ≠ 0 → (n • a = n • b ↔ a = b)- Defined in
- Mathlib.Algebra.Group.Torsion
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- Assumes
- AddMonoidIsAddTorsionFree
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.
- AddMonoidstatement and proof · cited by 2,864
- IsAddTorsionFreestatement and proof · cited by 155
- nsmul_right_injectiveproof · cited by 8
Cited by21
Results whose statement or proof uses this declaration.
- MvPowerSeries.coeff_expand_smulproof · cited by 7
- Ring.choose_zero_right'proof · cited by 7
- MvPolynomial.coeff_expand_smulproof · cited by 6
- Ring.choose_natCastproof · cited by 4
- Ring.choose_negproof · cited by 3
- nsmul_eq_zero_iff_rightproof · cited by 2
- Ring.multichoose_one_right'proof · cited by 2
- Ring.multichoose_succ_succproof · cited by 2
- Ring.multichoose_zero_right'proof · cited by 2
- AddCommGroup.nsmul_modEq_nsmulproof · cited by 1
- Ring.add_choose_eqproof · cited by 1
- Ring.multichoose_succ_neg_natCastproof · cited by 1