Theorems · Theorem · commutative algebra
Ring.ord_zero
∀ (R : Type u_1) [inst : CommRing R], Ring.ord R 0 = Module.length R R
The order of zero is Module.length R R. Use this when it is necessary to unfold the definition
of ord to avoid annoyances of working with R ⧸ Ideal.span {0} instead of R.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- RingHom.idproof · cited by 18,349
- CommRingstatement and proof · cited by 17,173
- ENatstatement · cited by 4,985
- LinearEquivproof · cited by 3,317
- HasQuotient.Quotientproof · cited by 2,301
- le_antisymmproof · cited by 2,068
- LinearEquiv.toLinearMapproof · cited by 1,171
- Ideal.spanproof · cited by 948
- LinearEquiv.injectiveproof · cited by 162
- LinearEquiv.surjectiveproof · cited by 66
- Module.lengthstatement · cited by 56
- Ring.ordstatement · cited by 28
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.