Theorems · Theorem · commutative algebra
Module.length_of_free
∀ (R : Type u_1) (M : Type u_2) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Free R M], Module.length R M = Cardinal.toENat (Module.rank R M) * Module.length R R
- Defined in
- Mathlib.RingTheory.Length
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 112 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites39
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Modulestatement and proof · cited by 20,661
- Semiringproof · cited by 13,802
- AddCommGroupstatement and proof · cited by 12,871
- AddCommMonoidproof · cited by 12,281
- Top.topproof · cited by 9,680
- Ringstatement and proof · cited by 7,463
- ENatstatement and proof · cited by 4,985
- Cardinalstatement and proof · cited by 2,598
- Nontrivialproof · cited by 2,416
- MulZeroClass.mul_zeroproof · cited by 2,091
- MulZeroClass.zero_mulproof · cited by 1,625
Cited by3
Results whose statement or proof uses this declaration.
- Module.length_eq_finrankproof · cited by 1
- Module.length_eq_rankproof · cited by 1
- Module.length_of_free_of_finiteproof · cited by 0