Documentation Verification Report

Cast

📁 Source: Mathlib/Algebra/Order/Ring/Cast.lean

Statistics

Metric	Count
Definitions `instAddCommGroupWithOne`, `instAddGroupWithOne`, `instIntCast`	3
Theorems `cast_abs`, `cast_le`, `cast_le_neg_one_of_neg`, `cast_le_neg_one_or_one_le_cast_of_ne_zero`, `cast_lt`, `cast_lt_zero`, `cast_max`, `cast_min`, `cast_mono`, `cast_natAbs`, `cast_nonneg`, `cast_nonneg_iff`, `cast_nonpos`, `cast_one_le_of_pos`, `cast_pos`, `cast_strictMono`, `nneg_mul_add_sq_of_abs_le_one`, `ofLex_intCast`, `toLex_intCast`	19
Total	22

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_abs` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `abs` `instLatticeInt` `instAddGroup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup`	—	`cast_max` `cast_neg`
`cast_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne`	—	`sub_nonneg` `covariant_swap_add_of_covariant_add` `cast_sub` `cast_nonneg_iff` `instAddLeftMono`
`cast_le_neg_one_of_neg` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`cast_one` `cast_neg` `cast_le` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero`
`cast_le_neg_one_or_one_le_cast_of_ne_zero` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`cast_le_neg_one_of_neg` `cast_one_le_of_pos` `Ne.lt_or_gt`
`cast_lt` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne`	—	`StrictMono.lt_iff_lt` `cast_strictMono`
`cast_lt_zero` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddCommGroupWithOne.toAddCommGroup`	—	`cast_zero` `cast_lt`
`cast_max` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Monotone.map_max` `cast_mono` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass`
`cast_min` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Monotone.map_min` `cast_mono` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass`
`cast_mono` 📖	mathematical	—	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne`	—	`CanLift.prf` `instCanLiftIntNatCastLeOfNat` `sub_nonneg` `covariant_swap_add_of_covariant_add` `instAddLeftMono` `cast_sub` `cast_natCast` `Nat.cast_nonneg'`
`cast_natAbs` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `AddGroupWithOne.toIntCast` `abs` `instLatticeInt` `instAddGroup`	—	`Nat.cast_natAbs`
`cast_nonneg` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddCommGroupWithOne.toAddCommGroup` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne`	—	`cast_natCast`
`cast_nonneg_iff` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddCommGroupWithOne.toAddCommGroup` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne`	—	`cast_natCast` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `lt_of_le_of_lt` `zero_lt_one` `cast_negSucc` `Nat.cast_add` `Nat.cast_one` `neg_add_rev` `covariant_swap_add_of_covariant_add` `LT.lt.not_ge`
`cast_nonpos` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddCommGroupWithOne.toAddCommGroup`	—	`cast_zero` `cast_le`
`cast_one_le_of_pos` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `AddGroupWithOne.toIntCast`	—	`Nat.cast_zero` `Nat.cast_one` `cast_one` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero`
`cast_pos` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddCommGroupWithOne.toAddCommGroup` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne`	—	`cast_zero` `cast_lt`
`cast_strictMono` 📖	mathematical	—	`StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne`	—	`strictMono_of_le_iff_le` `cast_le`
`nneg_mul_add_sq_of_abs_le_one` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `covariant_swap_add_of_covariant_add` `neg_le_of_abs_le` `cast_one_le_of_pos` `neg_add_cancel` `le_of_abs_le` `cast_le_neg_one_of_neg` `add_neg_cancel` `mul_add` `Distrib.leftDistribClass` `mul_nonneg_iff` `AddGroup.existsAddOfLE` `IsStrictOrderedRing.toMulPosStrictMono` `IsStrictOrderedRing.toPosMulStrictMono` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `lt_trichotomy` `Nat.cast_zero` `cast_zero` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `LT.lt.le` `instReflLe` `add_zero` `le_total`

Lex

Definitions

Name	Category	Theorems
`instAddCommGroupWithOne` 📖	CompOp	—
`instAddGroupWithOne` 📖	CompOp	—
`instIntCast` 📖	CompOp	2 math math: `ofLex_intCast`, `toLex_intCast`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofLex_intCast` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Lex` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex` `Lex.instIntCast`	—	—
`toLex_intCast` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Lex` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `Lex.instIntCast`	—	—

---

← Back to Index