Order

📁 Source: Mathlib/Data/Rat/Cast/Order.lean

Statistics

Metric	Count
Definitions `evalNNRatCast`, `evalRatCast`, `castOrderEmbedding`, `castOrderEmbedding`	4
Theorems `castOrderEmbedding_apply`, `cast_le`, `cast_le_natCast`, `cast_le_ofNat`, `cast_le_one`, `cast_lt`, `cast_lt_natCast`, `cast_lt_ofNat`, `cast_lt_one`, `cast_lt_zero`, `cast_max`, `cast_min`, `cast_mono`, `cast_nonpos`, `cast_pos`, `cast_strictMono`, `natCast_le_cast`, `natCast_lt_cast`, `not_cast_lt_zero`, `ofNat_le_cast`, `ofNat_lt_cast`, `one_le_cast`, `one_lt_cast`, `preimage_cast_Icc`, `preimage_cast_Ici`, `preimage_cast_Ico`, `preimage_cast_Iic`, `preimage_cast_Iio`, `preimage_cast_Ioc`, `preimage_cast_Ioi`, `preimage_cast_Ioo`, `preimage_cast_uIcc`, `preimage_cast_uIoc`, `castHom_rat`, `castOrderEmbedding_apply`, `cast_abs`, `cast_le`, `cast_le_intCast`, `cast_le_natCast`, `cast_lt`, `cast_lt_intCast`, `cast_lt_natCast`, `cast_lt_zero`, `cast_max`, `cast_min`, `cast_mono`, `cast_nonneg`, `cast_nonpos`, `cast_pos`, `cast_pos_of_pos`, `cast_strictMono`, `intCast_le_cast`, `intCast_lt_cast`, `natCast_le_cast`, `natCast_lt_cast`, `preimage_cast_Icc`, `preimage_cast_Ici`, `preimage_cast_Ico`, `preimage_cast_Iic`, `preimage_cast_Iio`, `preimage_cast_Ioc`, `preimage_cast_Ioi`, `preimage_cast_Ioo`, `preimage_cast_uIcc`, `preimage_cast_uIoc`	65
Total	69

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
`evalNNRatCast` 📖	CompOp	—
`evalRatCast` 📖	CompOp	—

NNRat

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` `NNRat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderNNRat` `RelEmbedding.instFunLike` `castOrderEmbedding` `cast` `DivisionSemiring.toNNRatCast` `Semifield.toDivisionSemiring`	—	—
`cast_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `cast` `DivisionSemiring.toNNRatCast` `Semifield.toDivisionSemiring` `NNRat` `instLinearOrderNNRat`	—	`OrderEmbedding.le_iff_le`
`cast_le_natCast` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `cast` `DivisionSemiring.toNNRatCast` `Semifield.toDivisionSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `NNRat` `instLinearOrderNNRat` `instSemifield`	—	`cast_le` `cast_natCast`
`cast_le_ofNat` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `cast` `DivisionSemiring.toNNRatCast` `Semifield.toDivisionSemiring` `NNRat` `instLinearOrderNNRat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `instSemifield`	—	`cast_le` `cast_ofNat`
`cast_le_one` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `cast` `DivisionSemiring.toNNRatCast` `Semifield.toDivisionSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `NNRat` `instLinearOrderNNRat` `instSemifield`	—	`Nat.cast_one` `cast_one`
`cast_lt` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `cast` `DivisionSemiring.toNNRatCast` `Semifield.toDivisionSemiring` `NNRat` `instLinearOrderNNRat`	—	`StrictMono.lt_iff_lt` `cast_strictMono`
`cast_lt_natCast` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `cast` `DivisionSemiring.toNNRatCast` `Semifield.toDivisionSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `NNRat` `instLinearOrderNNRat` `instSemifield`	—	`cast_lt` `cast_natCast`
`cast_lt_ofNat` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `cast` `DivisionSemiring.toNNRatCast` `Semifield.toDivisionSemiring` `NNRat` `instLinearOrderNNRat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `instSemifield`	—	`cast_lt` `cast_ofNat`
`cast_lt_one` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `cast` `DivisionSemiring.toNNRatCast` `Semifield.toDivisionSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `NNRat` `instLinearOrderNNRat` `instSemifield`	—	`Nat.cast_one` `cast_one`
`cast_lt_zero` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `cast` `DivisionSemiring.toNNRatCast` `Semifield.toDivisionSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `NNRat` `instLinearOrderNNRat` `instSemifield`	—	`Nat.cast_zero` `cast_zero`
`cast_max` 📖	mathematical	—	`cast` `DivisionSemiring.toNNRatCast` `Semifield.toDivisionSemiring` `NNRat` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderNNRat`	—	`Monotone.map_max` `cast_mono`
`cast_min` 📖	mathematical	—	`cast` `DivisionSemiring.toNNRatCast` `Semifield.toDivisionSemiring` `NNRat` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderNNRat`	—	`Monotone.map_min` `cast_mono`
`cast_mono` 📖	mathematical	—	`Monotone` `NNRat` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderNNRat` `cast` `DivisionSemiring.toNNRatCast` `Semifield.toDivisionSemiring`	—	`StrictMono.monotone` `cast_strictMono`
`cast_nonpos` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `cast` `DivisionSemiring.toNNRatCast` `Semifield.toDivisionSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `NNRat` `instLinearOrderNNRat` `instSemifield`	—	`Nat.cast_zero` `cast_zero`
`cast_pos` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `cast` `DivisionSemiring.toNNRatCast` `NNRat` `instLinearOrderNNRat` `instSemifield`	—	`Nat.cast_zero` `cast_zero`
`cast_strictMono` 📖	mathematical	—	`StrictMono` `NNRat` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderNNRat` `cast` `DivisionSemiring.toNNRatCast` `Semifield.toDivisionSemiring`	—	`cast_def` `div_lt_div_iff₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toIsOrderedRing` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Nat.cast_mul` `Nat.cast_lt` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toZeroLEOneClass` `lt_def`
`natCast_le_cast` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `cast` `DivisionSemiring.toNNRatCast` `NNRat` `instLinearOrderNNRat` `instSemifield`	—	`cast_le` `cast_natCast`
`natCast_lt_cast` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `cast` `DivisionSemiring.toNNRatCast` `NNRat` `instLinearOrderNNRat` `instSemifield`	—	`cast_lt` `cast_natCast`
`not_cast_lt_zero` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `cast` `DivisionSemiring.toNNRatCast` `Semifield.toDivisionSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring`	—	`Nat.cast_zero` `cast_zero` `not_lt_zero'`
`ofNat_le_cast` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `cast` `DivisionSemiring.toNNRatCast` `Semifield.toDivisionSemiring` `NNRat` `instLinearOrderNNRat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `instSemifield`	—	`cast_le` `cast_ofNat`
`ofNat_lt_cast` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `cast` `DivisionSemiring.toNNRatCast` `Semifield.toDivisionSemiring` `NNRat` `instLinearOrderNNRat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `instSemifield`	—	`cast_lt` `cast_ofNat`
`one_le_cast` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `cast` `DivisionSemiring.toNNRatCast` `NNRat` `instLinearOrderNNRat` `instSemifield`	—	`Nat.cast_one` `cast_one`
`one_lt_cast` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `cast` `DivisionSemiring.toNNRatCast` `NNRat` `instLinearOrderNNRat` `instSemifield`	—	`Nat.cast_one` `cast_one`
`preimage_cast_Icc` 📖	mathematical	—	`Set.preimage` `NNRat` `cast` `DivisionSemiring.toNNRatCast` `Semifield.toDivisionSemiring` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderNNRat`	—	`OrderEmbedding.preimage_Icc`
`preimage_cast_Ici` 📖	mathematical	—	`Set.preimage` `NNRat` `cast` `DivisionSemiring.toNNRatCast` `Semifield.toDivisionSemiring` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderNNRat`	—	`OrderEmbedding.preimage_Ici`
`preimage_cast_Ico` 📖	mathematical	—	`Set.preimage` `NNRat` `cast` `DivisionSemiring.toNNRatCast` `Semifield.toDivisionSemiring` `Set.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderNNRat`	—	`OrderEmbedding.preimage_Ico`
`preimage_cast_Iic` 📖	mathematical	—	`Set.preimage` `NNRat` `cast` `DivisionSemiring.toNNRatCast` `Semifield.toDivisionSemiring` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderNNRat`	—	`OrderEmbedding.preimage_Iic`
`preimage_cast_Iio` 📖	mathematical	—	`Set.preimage` `NNRat` `cast` `DivisionSemiring.toNNRatCast` `Semifield.toDivisionSemiring` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderNNRat`	—	`OrderEmbedding.preimage_Iio`
`preimage_cast_Ioc` 📖	mathematical	—	`Set.preimage` `NNRat` `cast` `DivisionSemiring.toNNRatCast` `Semifield.toDivisionSemiring` `Set.Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderNNRat`	—	`OrderEmbedding.preimage_Ioc`
`preimage_cast_Ioi` 📖	mathematical	—	`Set.preimage` `NNRat` `cast` `DivisionSemiring.toNNRatCast` `Semifield.toDivisionSemiring` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderNNRat`	—	`OrderEmbedding.preimage_Ioi`
`preimage_cast_Ioo` 📖	mathematical	—	`Set.preimage` `NNRat` `cast` `DivisionSemiring.toNNRatCast` `Semifield.toDivisionSemiring` `Set.Ioo` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderNNRat`	—	`OrderEmbedding.preimage_Ioo`
`preimage_cast_uIcc` 📖	mathematical	—	`Set.preimage` `NNRat` `cast` `DivisionSemiring.toNNRatCast` `Semifield.toDivisionSemiring` `Set.uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderNNRat`	—	`OrderEmbedding.preimage_uIcc`
`preimage_cast_uIoc` 📖	mathematical	—	`Set.preimage` `NNRat` `cast` `DivisionSemiring.toNNRatCast` `Semifield.toDivisionSemiring` `Set.uIoc` `instLinearOrderNNRat`	—	`OrderEmbedding.preimage_uIoc`

Rat

Definitions

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

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`castHom_rat` 📖	mathematical	—	`castHom` `instDivisionRing` `instCharZero` `RingHom.id` `Semiring.toNonAssocSemiring` `semiring`	—	`RingHom.ext` `instCharZero` `cast_id`
`castOrderEmbedding_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `RelEmbedding.instFunLike` `castOrderEmbedding` `DivisionRing.toRatCast` `Field.toDivisionRing`	—	—
`cast_abs` 📖	mathematical	—	`DivisionRing.toRatCast` `Field.toDivisionRing` `abs` `instLattice` `addGroup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing`	—	`cast_max` `cast_neg`
`cast_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionRing.toRatCast` `Field.toDivisionRing`	—	`OrderEmbedding.le_iff_le`
`cast_le_intCast` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionRing.toRatCast` `Field.toDivisionRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `DivisionRing.toRing`	—	`cast_le` `cast_intCast`
`cast_le_natCast` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionRing.toRatCast` `Field.toDivisionRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing`	—	`cast_le` `cast_natCast`
`cast_lt` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionRing.toRatCast` `Field.toDivisionRing`	—	`StrictMono.lt_iff_lt` `cast_strictMono`
`cast_lt_intCast` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionRing.toRatCast` `Field.toDivisionRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `DivisionRing.toRing`	—	`cast_lt` `cast_intCast`
`cast_lt_natCast` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionRing.toRatCast` `Field.toDivisionRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing`	—	`cast_lt` `cast_natCast`
`cast_lt_zero` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionRing.toRatCast` `Field.toDivisionRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`Nat.cast_zero` `cast_zero`
`cast_max` 📖	mathematical	—	`DivisionRing.toRatCast` `Field.toDivisionRing` `instSup` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Monotone.map_max` `cast_mono`
`cast_min` 📖	mathematical	—	`DivisionRing.toRatCast` `Field.toDivisionRing` `instInf` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Monotone.map_min` `cast_mono`
`cast_mono` 📖	mathematical	—	`Monotone` `instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionRing.toRatCast` `Field.toDivisionRing`	—	`StrictMono.monotone` `cast_strictMono`
`cast_nonneg` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `DivisionRing.toRatCast` `Field.toDivisionRing`	—	`Nat.cast_zero` `cast_zero`
`cast_nonpos` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionRing.toRatCast` `Field.toDivisionRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`Nat.cast_zero` `cast_zero`
`cast_pos` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `DivisionRing.toRatCast` `Field.toDivisionRing`	—	`Nat.cast_zero` `cast_zero`
`cast_pos_of_pos` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `DivisionRing.toRatCast` `Field.toDivisionRing`	—	`cast_def` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Int.cast_pos` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `num_pos` `Nat.cast_pos` `instNontrivialOfCharZero` `pos`
`cast_strictMono` 📖	mathematical	—	`StrictMono` `instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionRing.toRatCast` `Field.toDivisionRing`	—	`IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `instAddLeftMono` `cast_sub` `IsStrictOrderedRing.toCharZero` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `cast_pos_of_pos`
`intCast_le_cast` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `DivisionRing.toRatCast`	—	`cast_le` `cast_intCast`
`intCast_lt_cast` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `DivisionRing.toRatCast`	—	`cast_lt` `cast_intCast`
`natCast_le_cast` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `DivisionRing.toRatCast`	—	`cast_le` `cast_natCast`
`natCast_lt_cast` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `DivisionRing.toRatCast`	—	`cast_lt` `cast_natCast`
`preimage_cast_Icc` 📖	mathematical	—	`Set.preimage` `DivisionRing.toRatCast` `Field.toDivisionRing` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instPreorder`	—	`OrderEmbedding.preimage_Icc`
`preimage_cast_Ici` 📖	mathematical	—	`Set.preimage` `DivisionRing.toRatCast` `Field.toDivisionRing` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instPreorder`	—	`OrderEmbedding.preimage_Ici`
`preimage_cast_Ico` 📖	mathematical	—	`Set.preimage` `DivisionRing.toRatCast` `Field.toDivisionRing` `Set.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instPreorder`	—	`OrderEmbedding.preimage_Ico`
`preimage_cast_Iic` 📖	mathematical	—	`Set.preimage` `DivisionRing.toRatCast` `Field.toDivisionRing` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instPreorder`	—	`OrderEmbedding.preimage_Iic`
`preimage_cast_Iio` 📖	mathematical	—	`Set.preimage` `DivisionRing.toRatCast` `Field.toDivisionRing` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instPreorder`	—	`OrderEmbedding.preimage_Iio`
`preimage_cast_Ioc` 📖	mathematical	—	`Set.preimage` `DivisionRing.toRatCast` `Field.toDivisionRing` `Set.Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instPreorder`	—	`OrderEmbedding.preimage_Ioc`
`preimage_cast_Ioi` 📖	mathematical	—	`Set.preimage` `DivisionRing.toRatCast` `Field.toDivisionRing` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instPreorder`	—	`OrderEmbedding.preimage_Ioi`
`preimage_cast_Ioo` 📖	mathematical	—	`Set.preimage` `DivisionRing.toRatCast` `Field.toDivisionRing` `Set.Ioo` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instPreorder`	—	`OrderEmbedding.preimage_Ioo`
`preimage_cast_uIcc` 📖	mathematical	—	`Set.preimage` `DivisionRing.toRatCast` `Field.toDivisionRing` `Set.uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLattice`	—	`OrderEmbedding.preimage_uIcc`
`preimage_cast_uIoc` 📖	mathematical	—	`Set.preimage` `DivisionRing.toRatCast` `Field.toDivisionRing` `Set.uIoc` `linearOrder`	—	`OrderEmbedding.preimage_uIoc`

---

← Back to Index