Theorems · Definition · commutative algebra
Ideal.torsionOf
(R : Type u_1) → (M : Type u_2) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → M → Ideal R
The torsion ideal of x, containing all a such that a • x = 0.
- Defined in
- Mathlib.Algebra.Module.Torsion.Basic
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 26 from the axioms · uses propext, Quot.sound
- Assumes
- SemiringAddCommMonoidModule
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- Idealstatement · cited by 4,748
- LinearMap.kerproof · cited by 848
- LinearMap.toSpanSingletonproof · cited by 78
Cited by15
Results whose statement or proof uses this declaration.
- Ideal.quotTorsionOfEquivSpanSingletonstatement · cited by 3
- Ideal.mem_torsionOf_iffstatement · cited by 2
- Submodule.torsionBySet_eq_torsionBySet_spanproof · cited by 2
- Ideal.torsionOf_eq_span_pow_pOrderstatement and proof · cited by 2
- Ideal.torsionOf_zerostatement · cited by 2
- Module.p_pow_smul_liftproof · cited by 1
- Ideal.annihilator_span_singleton_eq_torsionOfstatement · cited by 1
- Module.torsion_by_prime_power_decompositionproof · cited by 1
- Ideal.iSupIndep.linearIndependent'statement and proof · cited by 0
- Ideal.quotTorsionOfEquivSpanSingleton_apply_mkstatement · cited by 0
- Module.annihilator_eq_iInf_torsionOfstatement and proof · cited by 0
- Ideal.torsionOf_eq_bot_iff_of_noZeroSMulDivisorsstatement and proof · cited by 0