Theorems · Definition · order theory
ENat.toNat
ℕ∞ → ℕ
Conversion of ℕ∞ to ℕ sending ∞ to 0.
- Defined in
- Mathlib.Data.ENat.Basic
- Cited by
- 143 results in Mathlib
- Foundations
- Depth 7 from the axioms, rests on 20 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ENatstatement · cited by 4,985
- WithTop.untopDproof · cited by 33
Cited by157
Results whose statement or proof uses this declaration.
- Set.ncardproof · cited by 344
- Polynomial.natTrailingDegreeproof · cited by 87
- Ideal.ramificationIdxproof · cited by 59
- Cardinal.toNat_liftproof · cited by 41
- SimpleGraph.distproof · cited by 40
- PowerSeries.IsWeierstrassDivisorAtproof · cited by 28
- PowerSeries.divXPowOrderproof · cited by 17
- PowerSeries.IsWeierstrassDivisorAt.modproof · cited by 16
- SimpleGraph.diamproof · cited by 15
- ENat.natCast_toNatstatement · cited by 11
- SimpleGraph.girthproof · cited by 11
- PowerSeries.IsWeierstrassDivisor.of_map_ne_zeroproof · cited by 11