Documentation Verification Report

Even

📁 Source: Mathlib/Algebra/Group/Subgroup/Even.lean

Statistics

Metric	Count
Definitions `even`, `even`, `even`, `square`, `square`, `square`	6
Theorems `coe_even`, `even_toAddSubmonoid`, `mem_even`, `coe_even`, `even_toSubsemigroup`, `mem_even`, `coe_even`, `mem_even`, `coe_square`, `mem_square`, `square_toSubmonoid`, `coe_square`, `mem_square`, `square_toSubsemigroup`, `coe_square`, `mem_square`	16
Total	22

AddSubgroup

Definitions

Name	Category	Theorems
`even` 📖	CompOp	3 math math: `coe_even`, `mem_even`, `even_toAddSubmonoid`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_even` 📖	mathematical	—	`SetLike.coe` `AddSubgroup` `AddCommGroup.toAddGroup` `instSetLike` `even` `setOf` `Even` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	—
`even_toAddSubmonoid` 📖	mathematical	—	`toAddSubmonoid` `AddCommGroup.toAddGroup` `even` `AddSubmonoid.even` `AddCommGroup.toAddCommMonoid`	—	—
`mem_even` 📖	mathematical	—	`AddSubgroup` `AddCommGroup.toAddGroup` `SetLike.instMembership` `instSetLike` `even` `Even` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	—

AddSubmonoid

Definitions

Name	Category	Theorems
`even` 📖	CompOp	4 math math: `coe_even`, `even_toSubsemigroup`, `AddSubgroup.even_toAddSubmonoid`, `mem_even`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_even` 📖	mathematical	—	`SetLike.coe` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instSetLike` `even` `setOf` `Even` `AddZero.toAdd` `AddZeroClass.toAddZero`	—	—
`even_toSubsemigroup` 📖	mathematical	—	`toAddSubsemigroup` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `even` `AddSubsemigroup.even` `AddCommMonoid.toAddCommSemigroup`	—	—
`mem_even` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `instSetLike` `even` `Even` `AddZero.toAdd` `AddZeroClass.toAddZero`	—	—

AddSubsemigroup

Definitions

Name	Category	Theorems
`even` 📖	CompOp	3 math math: `AddSubmonoid.even_toSubsemigroup`, `mem_even`, `coe_even`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_even` 📖	mathematical	—	`SetLike.coe` `AddSubsemigroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `instSetLike` `even` `setOf` `Even`	—	—
`mem_even` 📖	mathematical	—	`AddSubsemigroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `SetLike.instMembership` `instSetLike` `even` `Even`	—	—

Subgroup

Definitions

Name	Category	Theorems
`square` 📖	CompOp	3 math math: `mem_square`, `coe_square`, `square_toSubmonoid`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_square` 📖	mathematical	—	`SetLike.coe` `Subgroup` `CommGroup.toGroup` `instSetLike` `square` `setOf` `IsSquare` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—
`mem_square` 📖	mathematical	—	`Subgroup` `CommGroup.toGroup` `SetLike.instMembership` `instSetLike` `square` `IsSquare` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—
`square_toSubmonoid` 📖	mathematical	—	`toSubmonoid` `CommGroup.toGroup` `square` `Submonoid.square` `CommGroup.toCommMonoid`	—	—

Submonoid

Definitions

Name	Category	Theorems
`square` 📖	CompOp	4 math math: `mem_square`, `square_toSubsemigroup`, `coe_square`, `Subgroup.square_toSubmonoid`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_square` 📖	mathematical	—	`SetLike.coe` `Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instSetLike` `square` `setOf` `IsSquare` `MulOne.toMul` `MulOneClass.toMulOne`	—	—
`mem_square` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `instSetLike` `square` `IsSquare` `MulOne.toMul` `MulOneClass.toMulOne`	—	—
`square_toSubsemigroup` 📖	mathematical	—	`toSubsemigroup` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `square` `Subsemigroup.square` `CommMonoid.toCommSemigroup`	—	—

Subsemigroup

Definitions

Name	Category	Theorems
`square` 📖	CompOp	3 math math: `mem_square`, `Submonoid.square_toSubsemigroup`, `coe_square`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_square` 📖	mathematical	—	`SetLike.coe` `Subsemigroup` `CommMagma.toMul` `CommSemigroup.toCommMagma` `instSetLike` `square` `setOf` `IsSquare`	—	—
`mem_square` 📖	mathematical	—	`Subsemigroup` `CommMagma.toMul` `CommSemigroup.toCommMagma` `SetLike.instMembership` `instSetLike` `square` `IsSquare`	—	—

---

← Back to Index