Ring

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

Statistics

Metric	Count
Definitions	0
Theorems abs_cast, abs_ofNat, cast_eq_neg_cast, cast_max, cast_min, cast_nonneg, cast_pos, cast_tsub, mul_le_pow, neg_cast_eq_cast, ofNat_nonneg, ofNat_pos, ofNat_pos', two_mul_sq_add_one_le_two_pow_two_mul	14
Total	14

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_cast 📖	mathematical	—	abs AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne	—	abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid cast_nonneg
abs_ofNat 📖	mathematical	—	abs AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	abs_cast
cast_eq_neg_cast 📖	mathematical	—	AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	IsStrictOrderedRing.toCharZero
cast_max 📖	mathematical	—	AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Monotone.map_max mono_cast IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass
cast_min 📖	mathematical	—	AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Monotone.map_min mono_cast IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass
cast_nonneg 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	cast_nonneg' IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass
cast_pos 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	cast_pos' IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass NeZero.one
cast_tsub 📖	mathematical	—	AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	le_total cast_zero tsub_eq_zero_of_le mono_cast IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass le_iff_exists_add' instCanonicallyOrderedAdd add_tsub_cancel_right instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le instIsOrderedAddMonoid cast_add
mul_le_pow 📖	mathematical	—	Monoid.toNatPow instMonoid	—	MulZeroClass.mul_zero pow_zero instCanonicallyOrderedAdd pow_succ MulZeroClass.zero_mul add_zero zero_add add_comm add_assoc one_mul LE.le.trans' le_mul_of_one_le_right' instMulLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRing instNontrivial instAtLeastTwoHAddOfNat
neg_cast_eq_cast 📖	mathematical	—	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	IsStrictOrderedRing.toCharZero
ofNat_nonneg 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	ofNat_nonneg' IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass
ofNat_pos 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	ofNat_pos' IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass NeZero.one
ofNat_pos' 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid	—	cast_pos' NeZero.pos instCanonicallyOrderedAdd AtLeastTwo.toNeZero
two_mul_sq_add_one_le_two_pow_two_mul 📖	mathematical	—	Monoid.toNatPow instMonoid	—	zero_pow instCharZero instAtLeastTwoHAddOfNat MulZeroClass.mul_zero zero_add pow_zero add_pow_two one_pow mul_one add_assoc mul_add Distrib.leftDistribClass add_right_comm le_imp_le_of_le_of_le add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid le_refl pow_add pow_two mul_assoc mul_two add_le_add_right two_mul le_add_of_le_right instCanonicallyOrderedAdd mul_le_pow

---

← Back to Index