Documentation

Mathlib.Data.ENat.Lattice

Extended natural numbers form a complete linear order #

This instance is not in Data.ENat.Basic to avoid dependency on Finsets.