Documentation Verification Report

Opposite

📁 Source: Mathlib/Algebra/Group/Units/Opposite.lean

Statistics

Metric	Count
Definitions `opEquiv`, `opEquiv`	2
Theorems `coe_opEquiv_symm`, `coe_unop_opEquiv`, `op`, `unop`, `op`, `unop`, `coe_opEquiv_symm`, `coe_unop_opEquiv`, `isAddUnit_op`, `isAddUnit_unop`, `isUnit_op`, `isUnit_unop`	12
Total	14

AddUnits

Definitions

Name	Category	Theorems
`opEquiv` 📖	CompOp	2 math math: `coe_unop_opEquiv`, `coe_opEquiv_symm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_opEquiv_symm` 📖	mathematical	—	`val` `AddOpposite` `AddOpposite.instAddMonoid` `DFunLike.coe` `AddEquiv` `AddUnits` `AddOpposite.instAdd` `instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `opEquiv` `AddOpposite.op` `AddOpposite.unop`	—	—
`coe_unop_opEquiv` 📖	mathematical	—	`val` `AddOpposite.unop` `AddUnits` `DFunLike.coe` `AddEquiv` `AddOpposite` `AddOpposite.instAddMonoid` `instAdd` `AddOpposite.instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `opEquiv`	—	—

IsAddUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`op` 📖	mathematical	`IsAddUnit`	`AddOpposite` `AddOpposite.instAddMonoid` `AddOpposite.op`	—	—
`unop` 📖	mathematical	`IsAddUnit` `AddOpposite` `AddOpposite.instAddMonoid`	`AddOpposite.unop`	—	—

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`op` 📖	mathematical	`IsUnit`	`MulOpposite` `MulOpposite.instMonoid` `MulOpposite.op`	—	—
`unop` 📖	mathematical	`IsUnit` `MulOpposite` `MulOpposite.instMonoid`	`MulOpposite.unop`	—	—

Units

Definitions

Name	Category	Theorems
`opEquiv` 📖	CompOp	2 math math: `coe_unop_opEquiv`, `coe_opEquiv_symm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_opEquiv_symm` 📖	mathematical	—	`val` `MulOpposite` `MulOpposite.instMonoid` `DFunLike.coe` `MulEquiv` `Units` `MulOpposite.instMul` `instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `opEquiv` `MulOpposite.op` `MulOpposite.unop`	—	—
`coe_unop_opEquiv` 📖	mathematical	—	`val` `MulOpposite.unop` `Units` `DFunLike.coe` `MulEquiv` `MulOpposite` `MulOpposite.instMonoid` `instMul` `MulOpposite.instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `opEquiv`	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAddUnit_op` 📖	mathematical	—	`IsAddUnit` `AddOpposite` `AddOpposite.instAddMonoid` `AddOpposite.op`	—	`IsAddUnit.unop` `IsAddUnit.op`
`isAddUnit_unop` 📖	mathematical	—	`IsAddUnit` `AddOpposite.unop` `AddOpposite` `AddOpposite.instAddMonoid`	—	`IsAddUnit.op` `IsAddUnit.unop`
`isUnit_op` 📖	mathematical	—	`IsUnit` `MulOpposite` `MulOpposite.instMonoid` `MulOpposite.op`	—	`IsUnit.unop` `IsUnit.op`
`isUnit_unop` 📖	mathematical	—	`IsUnit` `MulOpposite.unop` `MulOpposite` `MulOpposite.instMonoid`	—	`IsUnit.op` `IsUnit.unop`

---

← Back to Index