ENat

📁 Source: Mathlib/SetTheory/Cardinal/ENat.lean

Statistics

Metric	Count
Definitions `gciENat`, `instCoeENat`, `ofENat`, `ofENatHom`, `toENat`, `toENatAux`	6
Theorems `aleph0_add_ofENat`, `aleph0_mul_ofENat`, `enat_gc`, `instCanLiftENatOfENatLeAleph0`, `lift_eq_ofENat`, `lift_le_ofENat`, `lift_lt_ofENat`, `lift_ofENat`, `nat_eq_ofENat`, `nat_le_ofENat`, `nat_lt_ofENat`, `ofENat_add`, `ofENat_add_aleph0`, `ofENat_eq_lift`, `ofENat_eq_nat`, `ofENat_eq_ofNat`, `ofENat_eq_one`, `ofENat_eq_zero`, `ofENat_inj`, `ofENat_injective`, `ofENat_le_aleph0`, `ofENat_le_lift`, `ofENat_le_nat`, `ofENat_le_ofENat`, `ofENat_le_ofENat_of_le`, `ofENat_le_ofNat`, `ofENat_le_one`, `ofENat_lt_aleph0`, `ofENat_lt_lift`, `ofENat_lt_nat`, `ofENat_lt_ofENat`, `ofENat_lt_ofENat_of_lt`, `ofENat_lt_ofNat`, `ofENat_mono`, `ofENat_mul`, `ofENat_mul_aleph0`, `ofENat_nat`, `ofENat_ofNat`, `ofENat_one`, `ofENat_pos`, `ofENat_strictMono`, `ofENat_toENat`, `ofENat_toENat_eq_self`, `ofENat_toENat_le`, `ofENat_top`, `ofENat_zero`, `ofNat_eq_ofENat`, `ofNat_le_ofENat`, `ofNat_lt_ofENat`, `one_eq_ofENat`, `one_le_ofENat`, `one_lt_ofENat`, `range_ofENat`, `toENatAux_eq_nat`, `toENatAux_eq_top`, `toENatAux_eq_zero`, `toENatAux_gc`, `toENatAux_le_nat`, `toENatAux_nat`, `toENatAux_ofENat`, `toENatAux_zero`, `toENat_comp_ofENat`, `toENat_congr`, `toENat_eq_iff_of_le_aleph0`, `toENat_eq_nat`, `toENat_eq_ofNat`, `toENat_eq_one`, `toENat_eq_top`, `toENat_eq_zero`, `toENat_injOn`, `toENat_le_iff_of_le_aleph0`, `toENat_le_iff_of_lt_aleph0`, `toENat_le_nat`, `toENat_le_ofNat`, `toENat_le_one`, `toENat_lift`, `toENat_lt_top`, `toENat_nat`, `toENat_ne_top`, `toENat_ofENat`, `toENat_strictMonoOn`, `zero_eq_ofENat`	82
Total	88

Cardinal

Definitions

Name	Category	Theorems
`gciENat` 📖	CompOp	—
`instCoeENat` 📖	CompOp	—
`ofENat` 📖	CompOp	62 math math: `ofENat_top`, `toNat_ofENat`, `ofENat_le_lift`, `lift_ofENat`, `lift_le_ofENat`, `Ideal.height_le_spanRank`, `ofENat_lt_lift`, `ofENat_eq_lift`, `ofENat_lt_ofNat`, `Ideal.height_le_iff_exists_minimalPrimes`, `ofENat_ofNat`, `ofENat_le_ofNat`, `toENat_ofENat`, `one_eq_ofENat`, `range_ofENat`, `ofENat_inj`, `ofENat_le_aleph0`, `ofENat_eq_ofNat`, `ofENat_mono`, `ofENat_le_ofENat_of_le`, `ofENat_lt_aleph0`, `nat_eq_ofENat`, `instCanLiftENatOfENatLeAleph0`, `lift_lt_ofENat`, `one_le_ofENat`, `ofENat_eq_zero`, `ofENat_add`, `ofENat_lt_ofENat_of_lt`, `ofENat_injective`, `ofENat_eq_one`, `ofENat_mul`, `ofENat_le_ofENat`, `ofNat_lt_ofENat`, `toENatAux_gc`, `ofENat_eq_nat`, `ofNat_le_ofENat`, `ofENat_lt_ofENat`, `ofENat_nat`, `ofENat_strictMono`, `ofENat_add_aleph0`, `one_lt_ofENat`, `ofENat_lt_nat`, `ofENat_le_one`, `ofENat_pos`, `ofENat_mul_aleph0`, `enat_gc`, `toENat_comp_ofENat`, `ofENat_toENat_le`, `zero_eq_ofENat`, `nat_le_ofENat`, `ofENat_toENat_eq_self`, `ofENat_toENat`, `aleph0_mul_ofENat`, `Ideal.exists_spanRank_eq_and_height_eq`, `lift_eq_ofENat`, `ofENat_le_nat`, `ofENat_zero`, `ofENat_one`, `ofNat_eq_ofENat`, `toENatAux_ofENat`, `aleph0_add_ofENat`, `nat_lt_ofENat`
`ofENatHom` 📖	CompOp	—
`toENat` 📖	CompOp	44 math math: `natCast_lt_toENat_iff`, `Set.toENat_cardinalMk_subtype`, `toENat_eq_natCast_iff`, `toENat_ofENat`, `Module.length_of_free`, `Submodule.spanRank_toENat_eq_iInf_encard`, `toENat_eq_zero`, `toENat_eq_ofNat`, `toENat_lt_natCast_iff`, `toENat_lift`, `toENat_le_ofNat`, `Ideal.height_le_spanRank_toENat_of_mem_minimal_primes`, `toNat_toENat`, `toENat_rank_span_set`, `toENat_strictMonoOn`, `Submodule.spanRank_toENat_eq_iInf_finset_card`, `continuum_toENat`, `toENat_le_iff_of_le_aleph0`, `toENat_eq_top`, `toENat_le_natCast_iff`, `Set.toENat_cardinalMk`, `enat_gc`, `toENat_le_nat`, `toENat_comp_ofENat`, `toENat_le_iff_of_lt_aleph0`, `ofENat_toENat_le`, `toENat_le_one`, `toENat_injOn`, `LinearIndepOn.encard_le_toENat_rank`, `toENat_eq_nat`, `ofENat_toENat_eq_self`, `ofENat_toENat`, `aleph_toENat`, `toENat_eq_iff_of_le_aleph0`, `Ideal.height_le_spanRank_toENat`, `natCast_eq_toENat_iff`, `toENat_nat`, `Matroid.toENat_cRank_eq`, `natCast_le_toENat_iff`, `Module.length_eq_rank`, `toENat_lt_top`, `toENat_congr`, `Matroid.toENat_cRk_eq`, `toENat_eq_one`
`toENatAux` 📖	CompOp	8 math math: `toENatAux_eq_top`, `toENatAux_eq_nat`, `toENatAux_nat`, `toENatAux_gc`, `toENatAux_zero`, `toENatAux_eq_zero`, `toENatAux_le_nat`, `toENatAux_ofENat`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aleph0_add_ofENat` 📖	mathematical	—	`Cardinal` `instAdd` `aleph0` `ofENat`	—	`ofENat_add`
`aleph0_mul_ofENat` 📖	mathematical	—	`Cardinal` `instMul` `aleph0` `ofENat`	—	`mul_comm` `ofENat_mul_aleph0`
`enat_gc` 📖	mathematical	—	`GaloisConnection` `ENat` `Cardinal` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `partialOrder` `ofENat` `DFunLike.coe` `OrderRingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `instCommSemiringENat` `OrderRingHom.instFunLike` `toENat`	—	`toENatAux_gc`
`instCanLiftENatOfENatLeAleph0` 📖	mathematical	—	`CanLift` `Cardinal` `ENat` `ofENat` `instLE` `aleph0`	—	`Set.ext_iff` `range_ofENat`
`lift_eq_ofENat` 📖	mathematical	—	`lift` `ofENat`	—	`lift_ofENat`
`lift_le_ofENat` 📖	mathematical	—	`Cardinal` `instLE` `lift` `ofENat`	—	`lift_ofENat` `lift_le`
`lift_lt_ofENat` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `lift` `ofENat`	—	`lift_ofENat` `lift_lt`
`lift_ofENat` 📖	mathematical	—	`lift` `ofENat`	—	`lift_natCast` `lift_aleph0`
`nat_eq_ofENat` 📖	mathematical	—	`Cardinal` `instNatCast` `ofENat` `ENat` `ENat.instNatCast`	—	—
`nat_le_ofENat` 📖	mathematical	—	`Cardinal` `instLE` `instNatCast` `ofENat` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast`	—	—
`nat_lt_ofENat` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instNatCast` `ofENat` `ENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast`	—	—
`ofENat_add` 📖	mathematical	—	`ofENat` `ENat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Cardinal` `instAdd`	—	`toENat_injOn` `toENat_ofENat` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `OrderRingHom.instRingHomClass`
`ofENat_add_aleph0` 📖	mathematical	—	`Cardinal` `instAdd` `ofENat` `aleph0`	—	`add_comm` `aleph0_add_ofENat`
`ofENat_eq_lift` 📖	mathematical	—	`ofENat` `lift`	—	`lift_ofENat`
`ofENat_eq_nat` 📖	mathematical	—	`ofENat` `Cardinal` `instNatCast` `ENat` `ENat.instNatCast`	—	—
`ofENat_eq_ofNat` 📖	mathematical	—	`ofENat` `ENat` `instOfNatAtLeastTwo` `ENat.instNatCast`	—	`ofENat_eq_nat`
`ofENat_eq_one` 📖	mathematical	—	`ofENat` `Cardinal` `instOne` `ENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`Nat.cast_one`
`ofENat_eq_zero` 📖	mathematical	—	`ofENat` `Cardinal` `instZero` `ENat` `instZeroENat`	—	`Nat.cast_zero`
`ofENat_inj` 📖	mathematical	—	`ofENat`	—	`ofENat_injective`
`ofENat_injective` 📖	mathematical	—	`ENat` `Cardinal` `ofENat`	—	`StrictMono.injective` `ofENat_strictMono`
`ofENat_le_aleph0` 📖	mathematical	—	`Cardinal` `instLE` `ofENat` `aleph0`	—	`ofENat_le_ofENat` `le_top`
`ofENat_le_lift` 📖	mathematical	—	`Cardinal` `instLE` `ofENat` `lift`	—	`lift_ofENat` `lift_le`
`ofENat_le_nat` 📖	mathematical	—	`Cardinal` `instLE` `ofENat` `instNatCast` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast`	—	—
`ofENat_le_ofENat` 📖	mathematical	—	`Cardinal` `instLE` `ofENat` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat`	—	`StrictMono.le_iff_le` `ofENat_strictMono`
`ofENat_le_ofENat_of_le` 📖	mathematical	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat`	`Cardinal` `instLE` `ofENat`	—	`ofENat_le_ofENat`
`ofENat_le_ofNat` 📖	mathematical	—	`Cardinal` `instLE` `ofENat` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `instOfNatAtLeastTwo` `ENat.instNatCast`	—	`ofENat_le_nat`
`ofENat_le_one` 📖	mathematical	—	`Cardinal` `instLE` `ofENat` `instOne` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`Nat.cast_one`
`ofENat_lt_aleph0` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `ofENat` `aleph0` `ENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `Top.top` `instTopENat`	—	`ofENat_lt_ofENat`
`ofENat_lt_lift` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `ofENat` `lift`	—	`lift_ofENat` `lift_lt`
`ofENat_lt_nat` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `ofENat` `instNatCast` `ENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast`	—	—
`ofENat_lt_ofENat` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `ofENat` `ENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat`	—	`StrictMono.lt_iff_lt` `ofENat_strictMono`
`ofENat_lt_ofENat_of_lt` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat`	`Cardinal` `partialOrder` `ofENat`	—	`ofENat_lt_ofENat`
`ofENat_lt_ofNat` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `ofENat` `ENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `instOfNatAtLeastTwo` `ENat.instNatCast`	—	`ofENat_lt_nat`
`ofENat_mono` 📖	mathematical	—	`Monotone` `ENat` `Cardinal` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `partialOrder` `ofENat`	—	`StrictMono.monotone` `ofENat_strictMono`
`ofENat_mul` 📖	mathematical	—	`ofENat` `ENat` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Cardinal` `instMul`	—	`toENat_injOn` `mul_le_mul'` `CanonicallyOrderedAdd.toMulLeftMono` `canonicallyOrderedAdd` `covariant_swap_mul_of_covariant_mul` `ofENat_le_aleph0` `aleph0_mul_aleph0` `toENat_ofENat` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `OrderRingHom.instRingHomClass`
`ofENat_mul_aleph0` 📖	mathematical	—	`Cardinal` `instMul` `ofENat` `aleph0`	—	`aleph0_mul_aleph0` `ofENat_nat` `nat_mul_aleph0` `Nat.cast_zero`
`ofENat_nat` 📖	mathematical	—	`ofENat` `ENat` `ENat.instNatCast` `Cardinal` `instNatCast`	—	—
`ofENat_ofNat` 📖	mathematical	—	`ofENat` `Cardinal` `instOfNatAtLeastTwo` `instNatCast`	—	—
`ofENat_one` 📖	mathematical	—	`ofENat` `ENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Cardinal` `instOne`	—	—
`ofENat_pos` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instZero` `ofENat` `ENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `instZeroENat`	—	`Nat.cast_zero`
`ofENat_strictMono` 📖	mathematical	—	`StrictMono` `ENat` `Cardinal` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `partialOrder` `ofENat`	—	`WithTop.strictMono_iff` `Nat.strictMono_cast` `addLeftMono` `IsOrderedRing.toZeroLEOneClass` `isOrderedRing` `instCharZero` `natCast_lt_aleph0`
`ofENat_toENat` 📖	mathematical	`Cardinal` `instLE` `aleph0`	`ofENat` `DFunLike.coe` `OrderRingHom` `ENat` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `PartialOrder.toPreorder` `partialOrder` `instCommSemiringENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `OrderRingHom.instFunLike` `toENat`	—	`ofENat_toENat_eq_self`
`ofENat_toENat_eq_self` 📖	mathematical	—	`ofENat` `DFunLike.coe` `OrderRingHom` `Cardinal` `ENat` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `PartialOrder.toPreorder` `partialOrder` `instCommSemiringENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `OrderRingHom.instFunLike` `toENat` `instLE` `aleph0`	—	`GaloisConnection.exists_eq_l` `enat_gc` `Set.ext_iff` `range_ofENat`
`ofENat_toENat_le` 📖	mathematical	—	`Cardinal` `instLE` `ofENat` `DFunLike.coe` `OrderRingHom` `ENat` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `PartialOrder.toPreorder` `partialOrder` `instCommSemiringENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `OrderRingHom.instFunLike` `toENat`	—	`GaloisConnection.l_u_le` `enat_gc`
`ofENat_top` 📖	mathematical	—	`ofENat` `Top.top` `ENat` `instTopENat` `aleph0`	—	—
`ofENat_zero` 📖	mathematical	—	`ofENat` `ENat` `instZeroENat` `Cardinal` `instZero`	—	—
`ofNat_eq_ofENat` 📖	mathematical	—	`ofENat` `ENat` `instOfNatAtLeastTwo` `ENat.instNatCast`	—	`nat_eq_ofENat`
`ofNat_le_ofENat` 📖	mathematical	—	`Cardinal` `instLE` `ofENat` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `instOfNatAtLeastTwo` `ENat.instNatCast`	—	`nat_le_ofENat`
`ofNat_lt_ofENat` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `ofENat` `ENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `instOfNatAtLeastTwo` `ENat.instNatCast`	—	`nat_lt_ofENat`
`one_eq_ofENat` 📖	mathematical	—	`Cardinal` `instOne` `ofENat` `ENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`Nat.cast_one`
`one_le_ofENat` 📖	mathematical	—	`Cardinal` `instLE` `instOne` `ofENat` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`Nat.cast_one`
`one_lt_ofENat` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instOne` `ofENat` `ENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`Nat.cast_one`
`range_ofENat` 📖	mathematical	—	`Set.range` `Cardinal` `ENat` `ofENat` `Set.Iic` `PartialOrder.toPreorder` `partialOrder` `aleph0`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `Set.range_subset_iff` `ofENat_le_aleph0` `LE.le.lt_or_eq` `CanLift.prf` `canLiftCardinalNat` `Set.mem_range_self`
`toENatAux_eq_nat` 📖	mathematical	—	`toENatAux` `ENat` `ENat.instNatCast` `Cardinal` `instNatCast`	—	`toENatAux_gc`
`toENatAux_eq_top` 📖	mathematical	`Cardinal` `instLE` `aleph0`	`toENatAux` `Top.top` `ENat` `instTopENat`	—	`Function.extend_apply'` `LE.le.not_gt` `natCast_lt_aleph0`
`toENatAux_eq_zero` 📖	mathematical	—	`toENatAux` `ENat` `instZeroENat` `Cardinal` `instZero`	—	`toENatAux_eq_nat`
`toENatAux_gc` 📖	mathematical	—	`GaloisConnection` `ENat` `Cardinal` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `partialOrder` `ofENat` `toENatAux`	—	`lt_or_ge` `CanLift.prf` `canLiftCardinalNat` `toENatAux_nat` `LE.le.trans` `ofENat_le_aleph0` `toENatAux_eq_top`
`toENatAux_le_nat` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `toENatAux` `ENat.instNatCast` `Cardinal` `instLE` `instNatCast`	—	`lt_or_ge` `CanLift.prf` `canLiftCardinalNat` `toENatAux_nat` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `addLeftMono` `isOrderedRing` `instCharZero` `toENatAux_eq_top` `LT.lt.trans_le` `natCast_lt_aleph0`
`toENatAux_nat` 📖	mathematical	—	`toENatAux` `Cardinal` `instNatCast` `ENat` `ENat.instNatCast`	—	`Function.Injective.extend_apply` `Nat.cast_injective` `instCharZero`
`toENatAux_ofENat` 📖	mathematical	—	`toENatAux` `ofENat`	—	`toENatAux_nat` `toENatAux_eq_top` `le_rfl`
`toENatAux_zero` 📖	mathematical	—	`toENatAux` `Cardinal` `instZero` `ENat` `instZeroENat`	—	`toENatAux_nat`
`toENat_comp_ofENat` 📖	mathematical	—	`ENat` `Cardinal` `DFunLike.coe` `OrderRingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `PartialOrder.toPreorder` `partialOrder` `instCommSemiringENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `OrderRingHom.instFunLike` `toENat` `ofENat`	—	`toENat_ofENat`
`toENat_congr` 📖	mathematical	—	`DFunLike.coe` `OrderRingHom` `Cardinal` `ENat` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `PartialOrder.toPreorder` `partialOrder` `instCommSemiringENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `OrderRingHom.instFunLike` `toENat`	—	`toENat_lift` `lift_mk_eq`
`toENat_eq_iff_of_le_aleph0` 📖	mathematical	`Cardinal` `instLE` `aleph0`	`DFunLike.coe` `OrderRingHom` `ENat` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `PartialOrder.toPreorder` `partialOrder` `instCommSemiringENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `OrderRingHom.instFunLike` `toENat`	—	`Set.InjOn.eq_iff` `StrictMonoOn.injOn` `toENat_strictMonoOn`
`toENat_eq_nat` 📖	mathematical	—	`DFunLike.coe` `OrderRingHom` `Cardinal` `ENat` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `PartialOrder.toPreorder` `partialOrder` `instCommSemiringENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `OrderRingHom.instFunLike` `toENat` `ENat.instNatCast` `instNatCast`	—	`toENatAux_eq_nat`
`toENat_eq_ofNat` 📖	mathematical	—	`DFunLike.coe` `OrderRingHom` `Cardinal` `ENat` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `PartialOrder.toPreorder` `partialOrder` `instCommSemiringENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `OrderRingHom.instFunLike` `toENat` `instOfNatAtLeastTwo` `instNatCast`	—	`toENat_eq_nat`
`toENat_eq_one` 📖	mathematical	—	`DFunLike.coe` `OrderRingHom` `Cardinal` `ENat` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `PartialOrder.toPreorder` `partialOrder` `instCommSemiringENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `OrderRingHom.instFunLike` `toENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `instOne`	—	`toENat_eq_nat`
`toENat_eq_top` 📖	mathematical	—	`DFunLike.coe` `OrderRingHom` `Cardinal` `ENat` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `PartialOrder.toPreorder` `partialOrder` `instCommSemiringENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `OrderRingHom.instFunLike` `toENat` `Top.top` `instTopENat` `instLE` `aleph0`	—	`GaloisConnection.u_eq_top` `enat_gc`
`toENat_eq_zero` 📖	mathematical	—	`DFunLike.coe` `OrderRingHom` `Cardinal` `ENat` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `PartialOrder.toPreorder` `partialOrder` `instCommSemiringENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `OrderRingHom.instFunLike` `toENat` `instZeroENat` `instZero`	—	`toENatAux_eq_zero`
`toENat_injOn` 📖	mathematical	—	`Set.InjOn` `Cardinal` `ENat` `DFunLike.coe` `OrderRingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `PartialOrder.toPreorder` `partialOrder` `instCommSemiringENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `OrderRingHom.instFunLike` `toENat` `Set.Iic` `aleph0`	—	`StrictMonoOn.injOn` `toENat_strictMonoOn`
`toENat_le_iff_of_le_aleph0` 📖	mathematical	`Cardinal` `instLE` `aleph0`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `DFunLike.coe` `OrderRingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `partialOrder` `instCommSemiringENat` `OrderRingHom.instFunLike` `toENat`	—	`CanLift.prf` `instCanLiftENatOfENatLeAleph0` `toENat_ofENat` `enat_gc`
`toENat_le_iff_of_lt_aleph0` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `aleph0`	`ENat` `Preorder.toLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `DFunLike.coe` `OrderRingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `instCommSemiringENat` `OrderRingHom.instFunLike` `toENat` `instLE`	—	`CanLift.prf` `canLiftCardinalNat` `toENat_nat`
`toENat_le_nat` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `DFunLike.coe` `OrderRingHom` `Cardinal` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `partialOrder` `instCommSemiringENat` `OrderRingHom.instFunLike` `toENat` `ENat.instNatCast` `instLE` `instNatCast`	—	`toENatAux_le_nat`
`toENat_le_ofNat` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `DFunLike.coe` `OrderRingHom` `Cardinal` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `partialOrder` `instCommSemiringENat` `OrderRingHom.instFunLike` `toENat` `instLE` `instOfNatAtLeastTwo` `instNatCast`	—	`toENat_le_nat`
`toENat_le_one` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `DFunLike.coe` `OrderRingHom` `Cardinal` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `partialOrder` `instCommSemiringENat` `OrderRingHom.instFunLike` `toENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `instLE` `instOne`	—	`toENat_le_nat`
`toENat_lift` 📖	mathematical	—	`DFunLike.coe` `OrderRingHom` `Cardinal` `ENat` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `PartialOrder.toPreorder` `partialOrder` `instCommSemiringENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `OrderRingHom.instFunLike` `toENat` `lift`	—	`le_total` `CanLift.prf` `instCanLiftENatOfENatLeAleph0` `lift_ofENat` `toENat_ofENat` `toENat_eq_top`
`toENat_lt_top` 📖	mathematical	—	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `DFunLike.coe` `OrderRingHom` `Cardinal` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `partialOrder` `instCommSemiringENat` `OrderRingHom.instFunLike` `toENat` `Top.top` `instTopENat` `aleph0`	—	—
`toENat_nat` 📖	mathematical	—	`DFunLike.coe` `OrderRingHom` `Cardinal` `ENat` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `PartialOrder.toPreorder` `partialOrder` `instCommSemiringENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `OrderRingHom.instFunLike` `toENat` `instNatCast` `ENat.instNatCast`	—	`map_natCast` `OrderRingHom.instRingHomClass`
`toENat_ne_top` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `aleph0`	—	—
`toENat_ofENat` 📖	mathematical	—	`DFunLike.coe` `OrderRingHom` `Cardinal` `ENat` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `PartialOrder.toPreorder` `partialOrder` `instCommSemiringENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `OrderRingHom.instFunLike` `toENat` `ofENat`	—	`toENatAux_ofENat`
`toENat_strictMonoOn` 📖	mathematical	—	`StrictMonoOn` `Cardinal` `ENat` `PartialOrder.toPreorder` `partialOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `DFunLike.coe` `OrderRingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `instCommSemiringENat` `OrderRingHom.instFunLike` `toENat` `Set.Iic` `aleph0`	—	`toENat_ofENat`
`zero_eq_ofENat` 📖	mathematical	—	`Cardinal` `instZero` `ofENat` `ENat` `instZeroENat`	—	`Nat.cast_zero`

---

← Back to Index