Documentation Verification Report

Submonoid

📁 Source: Mathlib/Algebra/Order/Monoid/Submonoid.lean

Statistics

Metric	Count
Definitions `nonneg`, `oneLE`	2
Theorems `coe_nonneg`, `mem_nonneg`, `toIsOrderedAddMonoid`, `toIsOrderedCancelAddMonoid`, `toIsOrderedAddMonoid`, `toIsOrderedCancelAddMonoid`, `coe_oneLE`, `mem_oneLE`, `toIsOrderedCancelMonoid`, `toIsOrderedMonoid`, `toIsOrderedCancelMonoid`, `toIsOrderedMonoid`	12
Total	14

AddSubmonoid

Definitions

Name	Category	Theorems
`nonneg` 📖	CompOp	9 math math: `AddGroupCone.nonneg_toAddSubmonoid`, `coe_nonneg`, `Rat.addSubmonoid_closure_range_pow`, `Rat.addSubmonoid_closure_range_mul_self`, `Int.addSubmonoid_closure_range_pow`, `mem_nonneg`, `Subsemiring.nonneg_toAddSubmonoid`, `Int.addSubmonoid_closure_range_mul_self`, `Subsemiring.coe_nonneg`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_nonneg` 📖	mathematical	—	`SetLike.coe` `AddSubmonoid` `AddMonoid.toAddZeroClass` `instSetLike` `nonneg` `Set.Ici` `AddZero.toZero` `AddZeroClass.toAddZero`	—	—
`mem_nonneg` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `instSetLike` `nonneg` `Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero`	—	—
`toIsOrderedAddMonoid` 📖	mathematical	—	`IsOrderedAddMonoid` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `instSetLike` `toAddCommMonoid` `Subtype.partialOrder`	—	`Function.Injective.isOrderedAddMonoid`
`toIsOrderedCancelAddMonoid` 📖	mathematical	—	`IsOrderedCancelAddMonoid` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `instSetLike` `toAddCommMonoid` `Subtype.partialOrder`	—	`Function.Injective.isOrderedCancelAddMonoid`

AddSubmonoidClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toIsOrderedAddMonoid` 📖	mathematical	—	`IsOrderedAddMonoid` `SetLike.instMembership` `toAddCommMonoid` `Subtype.partialOrder`	—	`Function.Injective.isOrderedAddMonoid`
`toIsOrderedCancelAddMonoid` 📖	mathematical	—	`IsOrderedCancelAddMonoid` `SetLike.instMembership` `toAddCommMonoid` `Subtype.partialOrder`	—	`Function.Injective.isOrderedCancelAddMonoid`

Submonoid

Definitions

Name	Category	Theorems
`oneLE` 📖	CompOp	3 math math: `GroupCone.oneLE_toSubmonoid`, `mem_oneLE`, `coe_oneLE`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_oneLE` 📖	mathematical	—	`SetLike.coe` `Submonoid` `Monoid.toMulOneClass` `instSetLike` `oneLE` `Set.Ici` `MulOne.toOne` `MulOneClass.toMulOne`	—	—
`mem_oneLE` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `instSetLike` `oneLE` `Preorder.toLE` `MulOne.toOne` `MulOneClass.toMulOne`	—	—
`toIsOrderedCancelMonoid` 📖	mathematical	—	`IsOrderedCancelMonoid` `Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `instSetLike` `toCommMonoid` `Subtype.partialOrder`	—	`Function.Injective.isOrderedCancelMonoid`
`toIsOrderedMonoid` 📖	mathematical	—	`IsOrderedMonoid` `Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `instSetLike` `toCommMonoid` `Subtype.partialOrder`	—	`Function.Injective.isOrderedMonoid`

SubmonoidClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toIsOrderedCancelMonoid` 📖	mathematical	—	`IsOrderedCancelMonoid` `SetLike.instMembership` `toCommMonoid` `Subtype.partialOrder`	—	`Function.Injective.isOrderedCancelMonoid`
`toIsOrderedMonoid` 📖	mathematical	—	`IsOrderedMonoid` `SetLike.instMembership` `toCommMonoid` `Subtype.partialOrder`	—	`Function.Injective.isOrderedMonoid`

---

← Back to Index