Documentation Verification Report

Cone

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

Statistics

Metric	Count
Definitions `AddGroupCone`, `instSetLike`, `nonneg`, `toAddSubmonoid`, `AddGroupConeClass`, `GroupCone`, `instSetLike`, `oneLE`, `toSubmonoid`, `GroupConeClass`, `IsMaxCone`, `IsMaxMulCone`, `mkOfAddGroupCone`, `mkOfGroupCone`, `mkOfAddGroupCone`, `mkOfGroupCone`, `instPartialOrderAddGroupCone`, `instPartialOrderGroupCone`	18
Theorems `coe_nonneg`, `eq_zero_of_mem_of_neg_mem'`, `instAddGroupConeClass`, `mem_nonneg`, `hasMemOrNegMem`, `isMaxCone`, `nonneg_toAddSubmonoid`, `eq_zero_of_mem_of_neg_mem`, `toAddSubmonoidClass`, `coe_oneLE`, `eq_one_of_mem_of_inv_mem'`, `instGroupConeClass`, `mem_oneLE`, `hasMemOrInvMem`, `isMaxMulCone`, `oneLE_toSubmonoid`, `eq_one_of_mem_of_inv_mem`, `toSubmonoidClass`, `mkOfCone`, `mkOfCone`, `mkOfAddGroupCone_le_iff`, `mkOfGroupCone_le_iff`	22
Total	40

AddGroupCone

Definitions

Name	Category	Theorems
`instSetLike` 📖	CompOp	5 math math: `nonneg.hasMemOrNegMem`, `instAddGroupConeClass`, `mem_nonneg`, `nonneg.isMaxCone`, `coe_nonneg`
`nonneg` 📖	CompOp	6 math math: `nonneg_toAddSubmonoid`, `nonneg.hasMemOrNegMem`, `mem_nonneg`, `RingCone.nonneg_toAddGroupCone`, `nonneg.isMaxCone`, `coe_nonneg`
`toAddSubmonoid` 📖	CompOp	1 math math: `nonneg_toAddSubmonoid`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_nonneg` 📖	mathematical	—	`SetLike.coe` `AddGroupCone` `instSetLike` `nonneg` `setOf` `Preorder.toLE` `PartialOrder.toPreorder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`eq_zero_of_mem_of_neg_mem'` 📖	mathematical	`Set` `Set.instMembership` `AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddSubmonoid.toAddSubsemigroup` `toAddSubmonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`NegZeroClass.toZero`	—	—
`instAddGroupConeClass` 📖	mathematical	—	`AddGroupConeClass` `AddGroupCone` `instSetLike`	—	`AddSubsemigroup.add_mem'` `AddSubmonoid.zero_mem'` `eq_zero_of_mem_of_neg_mem'`
`mem_nonneg` 📖	mathematical	—	`AddGroupCone` `SetLike.instMembership` `instSetLike` `nonneg` `Preorder.toLE` `PartialOrder.toPreorder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`nonneg_toAddSubmonoid` 📖	mathematical	—	`toAddSubmonoid` `nonneg` `AddSubmonoid.nonneg` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `PartialOrder.toPreorder` `IsOrderedAddMonoid.toAddLeftMono` `AddCommGroup.toAddCommMonoid`	—	—

AddGroupCone.nonneg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasMemOrNegMem` 📖	mathematical	—	`HasMemOrNegMem` `AddGroupCone` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddGroupCone.instSetLike` `AddGroupCone.nonneg` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`AddGroupCone.mem_nonneg` `Left.nonneg_neg_iff` `IsOrderedAddMonoid.toAddLeftMono` `le_total`
`isMaxCone` 📖	mathematical	—	`HasMemOrNegMem` `AddGroupCone` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddGroupCone.instSetLike` `AddGroupCone.nonneg` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`hasMemOrNegMem`

AddGroupConeClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_zero_of_mem_of_neg_mem` 📖	mathematical	`SetLike.instMembership` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`NegZeroClass.toZero`	—	—
`toAddSubmonoidClass` 📖	mathematical	—	`AddSubmonoidClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—

GroupCone

Definitions

Name	Category	Theorems
`instSetLike` 📖	CompOp	5 math math: `instGroupConeClass`, `coe_oneLE`, `mem_oneLE`, `oneLE.hasMemOrInvMem`, `oneLE.isMaxMulCone`
`oneLE` 📖	CompOp	5 math math: `oneLE_toSubmonoid`, `coe_oneLE`, `mem_oneLE`, `oneLE.hasMemOrInvMem`, `oneLE.isMaxMulCone`
`toSubmonoid` 📖	CompOp	1 math math: `oneLE_toSubmonoid`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_oneLE` 📖	mathematical	—	`SetLike.coe` `GroupCone` `instSetLike` `oneLE` `setOf` `Preorder.toLE` `PartialOrder.toPreorder` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	—	—
`eq_one_of_mem_of_inv_mem'` 📖	mathematical	`Set` `Set.instMembership` `Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Submonoid.toSubsemigroup` `toSubmonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	`InvOneClass.toOne`	—	—
`instGroupConeClass` 📖	mathematical	—	`GroupConeClass` `GroupCone` `instSetLike`	—	`Subsemigroup.mul_mem'` `Submonoid.one_mem'` `eq_one_of_mem_of_inv_mem'`
`mem_oneLE` 📖	mathematical	—	`GroupCone` `SetLike.instMembership` `instSetLike` `oneLE` `Preorder.toLE` `PartialOrder.toPreorder` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	—	—
`oneLE_toSubmonoid` 📖	mathematical	—	`toSubmonoid` `oneLE` `Submonoid.oneLE` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `PartialOrder.toPreorder` `IsOrderedMonoid.toMulLeftMono` `CommGroup.toCommMonoid`	—	—

GroupCone.oneLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasMemOrInvMem` 📖	mathematical	—	`HasMemOrInvMem` `GroupCone` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `GroupCone.instSetLike` `GroupCone.oneLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`IsOrderedMonoid.toMulLeftMono` `le_total`
`isMaxMulCone` 📖	mathematical	—	`HasMemOrInvMem` `GroupCone` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `GroupCone.instSetLike` `GroupCone.oneLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`hasMemOrInvMem`

GroupConeClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_one_of_mem_of_inv_mem` 📖	mathematical	`SetLike.instMembership` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	`InvOneClass.toOne`	—	—
`toSubmonoidClass` 📖	mathematical	—	`SubmonoidClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	—

IsOrderedAddMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mkOfCone` 📖	mathematical	—	`AddCommGroup.toAddCommMonoid` `PartialOrder.mkOfAddGroupCone`	—	`add_sub_add_right_eq_sub`

IsOrderedMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mkOfCone` 📖	mathematical	—	`CommGroup.toCommMonoid` `PartialOrder.mkOfGroupCone`	—	`mul_div_mul_right_eq_div`

LinearOrder

Definitions

Name	Category	Theorems
`mkOfAddGroupCone` 📖	CompOp	—
`mkOfGroupCone` 📖	CompOp	—

PartialOrder

Definitions

Name	Category	Theorems
`mkOfAddGroupCone` 📖	CompOp	3 math math: `IsOrderedAddMonoid.mkOfCone`, `IsOrderedRing.mkOfCone`, `mkOfAddGroupCone_le_iff`
`mkOfGroupCone` 📖	CompOp	2 math math: `mkOfGroupCone_le_iff`, `IsOrderedMonoid.mkOfCone`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mkOfAddGroupCone_le_iff` 📖	mathematical	—	`Preorder.toLE` `toPreorder` `mkOfAddGroupCone` `SetLike.instMembership` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—
`mkOfGroupCone_le_iff` 📖	mathematical	—	`Preorder.toLE` `toPreorder` `mkOfGroupCone` `SetLike.instMembership` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	—

(root)

Definitions

Name	Category	Theorems
`AddGroupCone` 📖	CompData	5 math math: `AddGroupCone.nonneg.hasMemOrNegMem`, `AddGroupCone.instAddGroupConeClass`, `AddGroupCone.mem_nonneg`, `AddGroupCone.nonneg.isMaxCone`, `AddGroupCone.coe_nonneg`
`AddGroupConeClass` 📖	CompData	2 math math: `AddGroupCone.instAddGroupConeClass`, `RingConeClass.toAddGroupConeClass`
`GroupCone` 📖	CompData	5 math math: `GroupCone.instGroupConeClass`, `GroupCone.coe_oneLE`, `GroupCone.mem_oneLE`, `GroupCone.oneLE.hasMemOrInvMem`, `GroupCone.oneLE.isMaxMulCone`
`GroupConeClass` 📖	CompData	1 math math: `GroupCone.instGroupConeClass`
`IsMaxCone` 📖	MathDef	—
`IsMaxMulCone` 📖	MathDef	—
`instPartialOrderAddGroupCone` 📖	CompOp	—
`instPartialOrderGroupCone` 📖	CompOp	—

---

← Back to Index