Structures · Algebra
IsAddTorsionFree
An additive monoid is torsion-free if scalar multiplication by every non-zero element n : ℕ is
injective.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument · adds nsmul_right_injective
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances14
- Int
- Nat
- Complex
- LocallyConstant
- PadicInt
- Finsupp
- FreeAddGroup
- AddLocalization
- Subtype
- Prod
- AddOpposite
- HasQuotient.Quotient
- Additive
- Multiset
How is a type an instance?
Loading the hierarchy index…
Assumed by135
- LieModule.chainTopCoeff
- LieModule.chainBotCoeff
- nsmul_right_inj
- LieModule.chainTop
- LieModule.coe_chainTop
- nsmul_right_injective
- not_isOfFinAddOrder_of_isAddTorsionFree
- LieModule.genWeightSpace_chainTopCoeff_add_one_nsmul_add
- LieModule.chainBot
- LieModule.chainTopCoeff_zero
- self_eq_neg
- Polynomial.derivative_eq_zero
- LieModule.genWeightSpace_add_chainTop
- Module.Basis.addSubgroupOfClosure
- RootPairing.nsmul_notMem_range_root
- LieModule.eventually_genWeightSpace_smul_add_eq_bot
- LieModule.chainBotCoeff_zero
- neg_eq_self
- Polynomial.degree_derivative
- RootPairing.coroot_eq_smul_coroot_iff
- LieModule.genWeightSpace_nsmul_add_ne_bot_of_le
- Polynomial.eq_C_of_derivative_eq_zero
- LieModule.coe_chainTop'
- LieAlgebra.LoopAlgebra.twoCochainOfBilinear
- Function.Odd.sum_eq_zero
- LieModule.chainBotCoeff_neg
- zsmul_right_inj
- DivisibleHull.coe_injective
- Function.Odd.finsetSum_eq_zero
- nsmul_eq_zero_iff
- Module.infinite_range_reflection_reflection_iterate_iff
- LieModule.exists_genWeightSpace_smul_add_eq_bot
- nsmul_eq_zero_iff_right
- CharZero.of_isAddTorsionFree
- IsAddTorsionFree.nsmul_right_injective
- LieModule.chainTopCoeff_neg
- Module.Basis.addSubgroupOfClosure_apply
- LieModule.chainTopCoeff_add_one
- Module.eq_of_mapsTo_reflection_of_mem
- LieModule.chainTopCoeff.congr_simp
- RootPairing.linearIndependent_of_add_mem_range_root
- IsAddLeftRegular.nsmul_injective
- LieAlgebra.Basis.A_diag_eq_two
- LieModule.chainTop.congr_simp
- IsOfFinAddOrder.eq_zero'
- two_nsmul_eq_zero
- RootPairing.linearIndependent_of_sub_mem_range_root
- Function.Odd.map_zero
- LieModule.exists₂_genWeightSpace_smul_add_eq_bot
- AddCommGroup.nsmul_modEq_nsmul
Ancestors0
No ancestors.