Structures · Algebra
Module.IsTorsionFree
An R-module M is torsion-free if scalar multiplication by an element r : R is injective if
multiplication (on R) by r is.
For domains, this is equivalent to the usual condition of r • m = 0 → r = 0 ∨ m = 0.
See smul_eq_zero.
- Defined in
- Mathlib.Algebra.Module.Torsion.Free
- Shape
- 2 explicit arguments · adds isSMulRegular
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances9
- Int
- Nat
- HahnSeries
- Localization
- NumberField.RingOfIntegers
- CyclotomicRing
- Localization.AtPrime
- Subtype
- MulOpposite
How is a type an instance?
Loading the hierarchy index…
Assumed by660
- Module.finrank_pos
- smul_eq_zero
- differentIdeal
- LieModule.chainTopCoeff
- Algebra.intNorm
- FractionalIdeal.extendedHom
- smul_left_injective
- smul_right_injective
- Ideal.relNorm
- LieModule.chainBotCoeff
- IsAddTorsionFree.of_isTorsionFree
- LieModule.chainTop
- Ideal.spanNorm
- smul_eq_zero_iff_right
- Polynomial.mem_rootSet
- Algebra.adjoin.powerBasis'
- Module.Basis.restrictScalars
- Polynomial.mem_rootSet_of_ne
- LinearEquiv.toSpanNonzeroSingleton
- meromorphicOrderAt_smul
- smul_eq_zero_iff_left
- LieModule.coe_chainTop
- smul_right_inj
- Algebra.intTrace
- minpoly.isIntegrallyClosed_dvd
- Submodule.finrank_eq_zero
- Module.finrank_pos_iff
- Polynomial.mem_aroots
- coeIdeal_differentIdeal
- KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk
- smul_ne_zero_iff
- Module.End.disjoint_genEigenspace
- ClassGroup.extendedHom
- RootPairing.pairing_eq_zero_iff
- LieModule.iSupIndep_genWeightSpace
- Module.Basis.restrictScalars_apply
- LieModule.genWeightSpace_chainTopCoeff_add_one_nsmul_add
- LinearIndepOn.singleton
- Module.IsTorsionFree.trans_faithfulSMul
- LieAlgebra.Basis.isCartanSubalgebra
- Algebra.algebraMap_intNorm_fractionRing
- Module.finrank_zero_iff
- Ideal.IsDedekindDomain.ramificationIdx'_ne_zero_of_liesOver
- IsRegular.isSMulRegular
- Module.Basis.mem_span_iff_repr_mem
- LieModule.chainBot
- smul_ne_zero
- FractionalIdeal.extendedHom_coeIdeal_eq_map
- LieModule.chainTopCoeff_zero
- Polynomial.aeval_algebraMap_eq_zero_iff
Ancestors0
No ancestors.