ToNat

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

Statistics

Metric	Count
Definitions `toNat`	1
Theorems `aleph0_toNat`, `cast_toNat_eq_iff_lt_aleph0`, `cast_toNat_of_aleph0_le`, `cast_toNat_of_lt_aleph0`, `mk_toNat_eq_card`, `mk_toNat_of_infinite`, `natCast_toNat_le`, `one_toNat`, `toNat_add`, `toNat_apply_of_aleph0_le`, `toNat_apply_of_lt_aleph0`, `toNat_congr`, `toNat_eq_iff`, `toNat_eq_ofNat`, `toNat_eq_one`, `toNat_eq_one_iff_unique`, `toNat_eq_zero`, `toNat_injOn`, `toNat_inj_of_lt_aleph0`, `toNat_le_iff_le_of_lt_aleph0`, `toNat_le_toNat`, `toNat_lift`, `toNat_lift_add_lift`, `toNat_lt_iff_lt_of_lt_aleph0`, `toNat_lt_toNat`, `toNat_monotoneOn`, `toNat_mul`, `toNat_natCast`, `toNat_ne_zero`, `toNat_ofENat`, `toNat_ofNat`, `toNat_pos`, `toNat_rightInverse`, `toNat_strictMonoOn`, `toNat_surjective`, `toNat_toENat`, `zero_toNat`	37
Total	38

Cardinal

Definitions

Name	Category	Theorems
`toNat` 📖	CompOp	44 math math: `toNat_ofENat`, `toNat_surjective`, `toNat_ofNat`, `toNat_eq_iff`, `toNat_congr`, `toNat_mul`, `toNat_apply_of_aleph0_le`, `Matrix.cRank_toNat_eq_rank`, `cast_toNat_eq_iff_lt_aleph0`, `Matrix.cRank_toNat_eq_finrank`, `toNat_monotoneOn`, `mk_toNat_eq_card`, `toNat_rightInverse`, `toNat_strictMonoOn`, `toNat_le_toNat`, `toNat_lt_iff_lt_of_lt_aleph0`, `toNat_lift`, `toNat_eq_one`, `toNat_toENat`, `IntermediateField.relfinrank_eq_toNat_relrank`, `Subfield.relfinrank_eq_toNat_relrank`, `mk_toNat_of_infinite`, `cast_toNat_of_aleph0_le`, `toNat_inj_of_lt_aleph0`, `toNat_injOn`, `toNat_le_iff_le_of_lt_aleph0`, `toNat_eq_one_iff_unique`, `toNat_lt_toNat`, `cast_toNat_of_lt_aleph0`, `toNat_eq_zero`, `Field.finSepDegree_eq`, `Field.finInsepDegree_def'`, `aleph0_toNat`, `toNat_natCast`, `toNat_apply_of_lt_aleph0`, `toNat_lift_add_lift`, `toNat_pos`, `toNat_add`, `zero_toNat`, `aleph_toNat`, `natCast_toNat_le`, `toNat_eq_ofNat`, `one_toNat`, `continuum_toNat`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aleph0_toNat` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Cardinal` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat` `aleph0`	—	`toNat_apply_of_aleph0_le` `le_rfl`
`cast_toNat_eq_iff_lt_aleph0` 📖	mathematical	—	`Cardinal` `instNatCast` `DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `aleph0`	—	`cast_toNat_of_lt_aleph0`
`cast_toNat_of_aleph0_le` 📖	mathematical	`Cardinal` `instLE` `aleph0`	`instNatCast` `DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat` `instZero`	—	`toNat_apply_of_aleph0_le` `Nat.cast_zero`
`cast_toNat_of_lt_aleph0` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `aleph0`	`instNatCast` `DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat`	—	`CanLift.prf` `canLiftCardinalNat` `toNat_natCast`
`mk_toNat_eq_card` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Cardinal` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat` `Fintype.card`	—	`mk_fintype` `toNat_natCast`
`mk_toNat_of_infinite` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Cardinal` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat`	—	`Nontrivial.to_nonempty` `Infinite.instNontrivial`
`natCast_toNat_le` 📖	mathematical	—	`Cardinal` `instLE` `instNatCast` `DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat`	—	`lt_or_ge` `cast_toNat_of_lt_aleph0` `toNat_apply_of_aleph0_le` `Nat.cast_zero` `canonicallyOrderedAdd`
`one_toNat` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Cardinal` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat` `instOne`	—	`map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass`
`toNat_add` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `aleph0`	`DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat` `instAdd`	—	`CanLift.prf` `canLiftCardinalNat` `toNat_natCast`
`toNat_apply_of_aleph0_le` 📖	mathematical	`Cardinal` `instLE` `aleph0`	`DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat`	—	—
`toNat_apply_of_lt_aleph0` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `aleph0`	`DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat` `instNatCast` `lt_aleph0`	—	`Nat.cast_injective` `instCharZero` `lt_aleph0` `cast_toNat_of_lt_aleph0`
`toNat_congr` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Cardinal` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat`	—	`toNat_lift` `lift_mk_eq`
`toNat_eq_iff` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Cardinal` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat` `instNatCast`	—	`toNat_toENat` `ENat.toNat_eq_iff` `toENat_eq_nat`
`toNat_eq_ofNat` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Cardinal` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat` `instOfNatAtLeastTwo` `instNatCast`	—	`toNat_eq_iff` `OfNat.ofNat_ne_zero` `Nat.instCharZero`
`toNat_eq_one` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Cardinal` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat` `instOne`	—	`toNat_eq_iff` `one_ne_zero` `Nat.cast_one`
`toNat_eq_one_iff_unique` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Cardinal` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat`	—	`toNat_eq_one` `eq_one_iff_unique`
`toNat_eq_zero` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Cardinal` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat` `instZero` `instLE` `aleph0`	—	`toNat_toENat` `ENat.toNat_eq_zero` `toENat_eq_zero` `toENat_eq_top`
`toNat_injOn` 📖	mathematical	—	`Set.InjOn` `Cardinal` `DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat` `Set.Iio` `PartialOrder.toPreorder` `partialOrder` `aleph0`	—	`StrictMonoOn.injOn` `toNat_strictMonoOn`
`toNat_inj_of_lt_aleph0` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `aleph0`	`DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat`	—	`Set.InjOn.eq_iff` `toNat_injOn`
`toNat_le_iff_le_of_lt_aleph0` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `aleph0`	`DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat` `instLE`	—	`StrictMonoOn.le_iff_le` `toNat_strictMonoOn`
`toNat_le_toNat` 📖	mathematical	`Cardinal` `instLE` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `aleph0`	`DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat`	—	`toNat_monotoneOn` `LE.le.trans_lt`
`toNat_lift` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Cardinal` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat` `lift`	—	`toENat_lift`
`toNat_lift_add_lift` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `aleph0`	`DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat` `instAdd` `lift`	—	`toNat_add` `toNat_lift`
`toNat_lt_iff_lt_of_lt_aleph0` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `aleph0`	`DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat`	—	`StrictMonoOn.lt_iff_lt` `toNat_strictMonoOn`
`toNat_lt_toNat` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `aleph0`	`DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat`	—	`toNat_strictMonoOn` `LT.lt.trans`
`toNat_monotoneOn` 📖	mathematical	—	`MonotoneOn` `Cardinal` `PartialOrder.toPreorder` `partialOrder` `Nat.instPreorder` `DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat` `Set.Iio` `aleph0`	—	`StrictMonoOn.monotoneOn` `toNat_strictMonoOn`
`toNat_mul` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Cardinal` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat` `instMul`	—	`map_mul` `MonoidHomClass.toMulHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass`
`toNat_natCast` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Cardinal` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat` `instNatCast`	—	`toNat_ofENat`
`toNat_ne_zero` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `aleph0`	—	—
`toNat_ofENat` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Cardinal` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat` `ofENat` `ENat.toNat`	—	`toENat_ofENat`
`toNat_ofNat` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Cardinal` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat`	—	`toNat_natCast`
`toNat_pos` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Cardinal` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `aleph0`	—	`pos_iff_ne_zero` `Nat.instCanonicallyOrderedAdd` `toNat_ne_zero`
`toNat_rightInverse` 📖	mathematical	—	`Cardinal` `instNatCast` `DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat`	—	`toNat_natCast`
`toNat_strictMonoOn` 📖	mathematical	—	`StrictMonoOn` `Cardinal` `PartialOrder.toPreorder` `partialOrder` `Nat.instPreorder` `DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat` `Set.Iio` `aleph0`	—	`toNat_natCast` `addLeftMono` `IsOrderedRing.toZeroLEOneClass` `isOrderedRing` `instCharZero`
`toNat_surjective` 📖	mathematical	—	`Cardinal` `DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat`	—	`toNat_rightInverse`
`toNat_toENat` 📖	mathematical	—	`ENat.toNat` `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` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat`	—	—
`zero_toNat` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Cardinal` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat` `instZero`	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass`

---

← Back to Index