Documentation Verification Report

Cone

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

Statistics

Metric	Count
Definitions `RingCone`, `instSetLike`, `nonneg`, `toAddGroupCone`, `toSubsemiring`, `RingConeClass`, `instPartialOrderRingCone`	7
Theorems `mkOfCone`, `coe_nonneg`, `coe_set_mk`, `eq_zero_of_mem_of_neg_mem'`, `instRingConeClass`, `mem_mk`, `mem_nonneg`, `hasMemOrNegMem`, `isMaxCone`, `nonneg_toAddGroupCone`, `nonneg_toSubsemiring`, `toAddGroupConeClass`, `toSubmonoidClass`, `toSubsemiringClass`	14
Total	21

IsOrderedRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mkOfCone` 📖	mathematical	—	`IsOrderedRing` `Ring.toSemiring` `PartialOrder.mkOfAddGroupCone` `Ring.toAddCommGroup` `RingConeClass.toAddGroupConeClass`	—	`of_mul_nonneg` `RingConeClass.toAddGroupConeClass` `IsOrderedAddMonoid.mkOfCone` `sub_zero` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `RingConeClass.toSubsemiringClass` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubsemiringClass.toSubmonoidClass`

RingCone

Definitions

Name	Category	Theorems
`instSetLike` 📖	CompOp	7 math math: `coe_set_mk`, `nonneg.isMaxCone`, `mem_nonneg`, `instRingConeClass`, `mem_mk`, `nonneg.hasMemOrNegMem`, `coe_nonneg`
`nonneg` 📖	CompOp	6 math math: `nonneg.isMaxCone`, `mem_nonneg`, `nonneg_toSubsemiring`, `nonneg.hasMemOrNegMem`, `nonneg_toAddGroupCone`, `coe_nonneg`
`toAddGroupCone` 📖	CompOp	1 math math: `nonneg_toAddGroupCone`
`toSubsemiring` 📖	CompOp	1 math math: `nonneg_toSubsemiring`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_nonneg` 📖	mathematical	—	`SetLike.coe` `RingCone` `instSetLike` `nonneg` `setOf` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—
`coe_set_mk` 📖	mathematical	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	`SetLike.coe` `RingCone` `instSetLike` `Subsemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Subsemiring.instSetLike`	—	—
`eq_zero_of_mem_of_neg_mem'` 📖	mathematical	`Set` `Set.instMembership` `Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Submonoid.toSubsemigroup` `Subsemiring.toSubmonoid` `toSubsemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	`NegZeroClass.toZero`	—	—
`instRingConeClass` 📖	mathematical	—	`RingConeClass` `RingCone` `instSetLike`	—	`Subsemiring.add_mem'` `Subsemiring.zero_mem'` `eq_zero_of_mem_of_neg_mem'` `Subsemigroup.mul_mem'` `Submonoid.one_mem'`
`mem_mk` 📖	mathematical	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	`RingCone` `SetLike.instMembership` `instSetLike` `Subsemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Subsemiring.instSetLike`	—	—
`mem_nonneg` 📖	mathematical	—	`RingCone` `SetLike.instMembership` `instSetLike` `nonneg` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—
`nonneg_toAddGroupCone` 📖	mathematical	—	`toAddGroupCone` `nonneg` `AddGroupCone.nonneg` `Ring.toAddCommGroup` `IsOrderedRing.toIsOrderedAddMonoid` `Ring.toSemiring`	—	—
`nonneg_toSubsemiring` 📖	mathematical	—	`toSubsemiring` `nonneg` `Subsemiring.nonneg` `Ring.toSemiring`	—	—

RingCone.nonneg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasMemOrNegMem` 📖	mathematical	—	`HasMemOrNegMem` `RingCone` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `RingCone.instSetLike` `RingCone.nonneg` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`HasMemOrNegMem.mem_or_neg_mem` `IsOrderedRing.toIsOrderedAddMonoid` `AddGroupCone.nonneg.hasMemOrNegMem`
`isMaxCone` 📖	mathematical	—	`HasMemOrNegMem` `RingCone` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `RingCone.instSetLike` `RingCone.nonneg` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`hasMemOrNegMem`

RingConeClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toAddGroupConeClass` 📖	mathematical	—	`AddGroupConeClass` `Ring.toAddCommGroup`	—	—
`toSubmonoidClass` 📖	mathematical	—	`SubmonoidClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring`	—	—
`toSubsemiringClass` 📖	mathematical	—	`SubsemiringClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring`	—	`toSubmonoidClass` `AddGroupConeClass.toAddSubmonoidClass` `toAddGroupConeClass`

(root)

Definitions

Name	Category	Theorems
`RingCone` 📖	CompData	7 math math: `RingCone.coe_set_mk`, `RingCone.nonneg.isMaxCone`, `RingCone.mem_nonneg`, `RingCone.instRingConeClass`, `RingCone.mem_mk`, `RingCone.nonneg.hasMemOrNegMem`, `RingCone.coe_nonneg`
`RingConeClass` 📖	CompData	1 math math: `RingCone.instRingConeClass`
`instPartialOrderRingCone` 📖	CompOp	—

---

← Back to Index