Basic

📁 Source: Mathlib/Data/Nat/Cast/Order/Basic.lean

Statistics

Metric	Count
Definitions `castOrderEmbedding`	1
Theorems `castOrderEmbedding_apply`, `cast_add_one_pos`, `cast_le`, `cast_le_ofNat`, `cast_le_one`, `cast_lt`, `cast_lt_ofNat`, `cast_lt_one`, `cast_nonneg'`, `cast_nonpos`, `cast_pos'`, `mono_cast`, `not_ofNat_le_one`, `not_ofNat_lt_one`, `ofNat_le`, `ofNat_le_cast`, `ofNat_lt`, `ofNat_lt_cast`, `ofNat_nonneg'`, `one_le_cast`, `one_le_cast_iff_ne_zero`, `one_le_ofNat`, `one_lt_cast`, `one_lt_ofNat`, `strictMono_cast`, `nat_of_injective`, `instNontrivialOfCharZero`	27
Total	28

Nat

Definitions

Name	Category	Theorems
`castOrderEmbedding` 📖	CompOp	1 math math: `castOrderEmbedding_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`castOrderEmbedding_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `RelEmbedding.instFunLike` `castOrderEmbedding` `AddMonoidWithOne.toNatCast`	—	—
`cast_add_one_pos` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddMonoidWithOne.toNatCast` `AddMonoidWithOne.toOne`	—	`LT.lt.trans_le` `zero_lt_one` `cast_one` `cast_add` `Monotone.imp` `mono_cast`
`cast_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddMonoidWithOne.toNatCast`	—	`StrictMono.le_iff_le` `strictMono_cast`
`cast_le_ofNat` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddMonoidWithOne.toNatCast`	—	`cast_le`
`cast_le_one` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddMonoidWithOne.toNatCast` `AddMonoidWithOne.toOne`	—	`cast_one` `cast_le`
`cast_lt` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddMonoidWithOne.toNatCast`	—	`StrictMono.lt_iff_lt` `strictMono_cast`
`cast_lt_ofNat` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddMonoidWithOne.toNatCast`	—	`cast_lt`
`cast_lt_one` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddMonoidWithOne.toNatCast` `AddMonoidWithOne.toOne`	—	`cast_one` `cast_lt`
`cast_nonneg'` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddMonoidWithOne.toNatCast`	—	`mono_cast` `cast_zero`
`cast_nonpos` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddMonoidWithOne.toNatCast` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid`	—	`cast_zero`
`cast_pos'` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddMonoidWithOne.toNatCast`	—	`cast_zero` `cast_add` `cast_one`
`mono_cast` 📖	mathematical	—	`Monotone` `instPreorder` `PartialOrder.toPreorder` `AddMonoidWithOne.toNatCast`	—	`monotone_nat_of_le_succ` `cast_succ` `le_add_of_nonneg_right` `zero_le_one`
`not_ofNat_le_one` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddMonoidWithOne.toOne`	—	`Iff.not` `cast_le_one` `not_le` `AtLeastTwo.one_lt`
`not_ofNat_lt_one` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddMonoidWithOne.toOne`	—	`le_of_lt` `not_ofNat_le_one`
`ofNat_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder`	—	`cast_le`
`ofNat_le_cast` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddMonoidWithOne.toNatCast`	—	`cast_le`
`ofNat_lt` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder`	—	`cast_lt`
`ofNat_lt_cast` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddMonoidWithOne.toNatCast`	—	`cast_lt`
`ofNat_nonneg'` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid`	—	`cast_nonneg'`
`one_le_cast` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddMonoidWithOne.toOne` `AddMonoidWithOne.toNatCast`	—	`cast_one` `cast_le`
`one_le_cast_iff_ne_zero` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddMonoidWithOne.toOne` `AddMonoidWithOne.toNatCast`	—	`one_le_cast`
`one_le_ofNat` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddMonoidWithOne.toOne`	—	`one_le_cast` `NeZero.one_le` `AtLeastTwo.toNeZero`
`one_lt_cast` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddMonoidWithOne.toOne` `AddMonoidWithOne.toNatCast`	—	`cast_one` `cast_lt`
`one_lt_ofNat` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddMonoidWithOne.toOne`	—	`one_lt_cast` `AtLeastTwo.one_lt`
`strictMono_cast` 📖	mathematical	—	`StrictMono` `instPreorder` `PartialOrder.toPreorder` `AddMonoidWithOne.toNatCast`	—	`Monotone.strictMono_of_injective` `mono_cast` `cast_injective`

NeZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nat_of_injective` 📖	mathematical	`DFunLike.coe`	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`natCast_ne` `map_natCast` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNontrivialOfCharZero` 📖	mathematical	—	`Nontrivial`	—	`Nat.cast_ne_zero` `Nat.cast_one`

---

← Back to Index