Theorems · Definition · commutative algebra
Module.length
(R : Type u_1) → (M : Type u_2) → [inst : Ring R] → [inst_1 : AddCommGroup M] → [Module R M] → ℕ∞
The length of a module, defined as the krull dimension of its submodule lattice.
- Defined in
- Mathlib.RingTheory.Length
- Cited by
- 56 results in Mathlib
- Foundations
- Depth 37 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- RingAddCommGroupModule
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- AddCommGroupstatement and proof · cited by 12,871
- Ringstatement and proof · cited by 7,463
- Submoduleproof · cited by 7,192
- ENatstatement · cited by 4,985
- Order.krullDimproof · cited by 82
- WithBot.unbotproof · cited by 23
Cited by58
Results whose statement or proof uses this declaration.
- Ideal.ramificationIdxproof · cited by 59
- Ring.ordproof · cited by 28
- Module.coe_lengthstatement · cited by 10
- Module.length_eq_zerostatement · cited by 9
- Module.length_ne_top_iffstatement and proof · cited by 8
- LinearEquiv.length_eqstatement and proof · cited by 7
- Ideal.ramificationIdx_defstatement · cited by 6
- Ideal.ramificationIdx_eqstatement and proof · cited by 6
- Module.length_eq_add_of_exactstatement and proof · cited by 6
- Ideal.ramificationIdx_eq_one_iffproof · cited by 4
- Module.length_compositionSeriesstatement · cited by 4
- Module.length_eq_of_surjectivestatement and proof · cited by 4