Documentation Verification Report

Basic

📁 Source: Mathlib/Algebra/Group/Invertible/Basic.lean

Statistics

Metric	Count
Definitions `map`, `mulLeft`, `mulRight`, `ofLeftInverse`, `invertible`, `invertible`, `invertibleEquivOfLeftInverse`, `invertibleOfInvertibleMul`, `invertibleOfMulInvertible`, `invertibleOfPowEqOne`, `invertiblePow`, `unitOfInvertible`	12
Theorems `invOf_left`, `invOf_right`, `mulLeft_apply`, `mulLeft_symm_apply`, `mulRight_apply`, `mulRight_symm_apply`, `ofLeftInverse_invOf`, `nonempty_invertible`, `commute_invOf`, `invOf_pow`, `invOf_units`, `invertibleEquivOfLeftInverse_apply`, `invertibleEquivOfLeftInverse_symm_apply`, `isUnit_of_invertible`, `map_invOf`, `nonempty_invertible_iff_isUnit`, `val_inv_unitOfInvertible`, `val_unitOfInvertible`	18
Total	30

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`invOf_left` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Invertible.invOf` `MulOne.toOne`	—	`mul_assoc` `mul_invOf_self'` `mul_one` `eq` `invOf_mul_cancel_left'`
`invOf_right` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Invertible.invOf` `MulOne.toOne`	—	`mul_assoc` `invOf_mul_cancel_left'` `eq` `mul_invOf_self'` `mul_one`

Invertible

Definitions

Name	Category	Theorems
`map` 📖	CompOp	3 math math: `ExteriorAlgebra.invertibleAlgebraMapEquiv_apply_invOf`, `ofLeftInverse_invOf`, `invertibleEquivOfLeftInverse_symm_apply`
`mulLeft` 📖	CompOp	2 math math: `mulLeft_apply`, `mulLeft_symm_apply`
`mulRight` 📖	CompOp	2 math math: `mulRight_apply`, `mulRight_symm_apply`
`ofLeftInverse` 📖	CompOp	2 math math: `invertibleEquivOfLeftInverse_apply`, `ofLeftInverse_invOf`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mulLeft_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Invertible` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne` `EquivLike.toFunLike` `Equiv.instEquivLike` `mulLeft` `invertibleMul`	—	—
`mulLeft_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Invertible` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `mulLeft` `invertibleOfInvertibleMul`	—	—
`mulRight_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Invertible` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne` `EquivLike.toFunLike` `Equiv.instEquivLike` `mulRight` `invertibleMul`	—	—
`mulRight_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Invertible` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `mulRight` `invertibleOfMulInvertible`	—	—
`ofLeftInverse_invOf` 📖	mathematical	`DFunLike.coe`	`invOf` `MulOne.toMul` `MulOneClass.toMulOne` `MulOne.toOne` `ofLeftInverse` `map`	—	—

IsUnit

Definitions

Name	Category	Theorems
`invertible` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nonempty_invertible` 📖	mathematical	`IsUnit`	`Invertible` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	—

Units

Definitions

Name	Category	Theorems
`invertible` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`invertibleEquivOfLeftInverse` 📖	CompOp	2 math math: `invertibleEquivOfLeftInverse_apply`, `invertibleEquivOfLeftInverse_symm_apply`
`invertibleOfInvertibleMul` 📖	CompOp	1 math math: `Invertible.mulLeft_symm_apply`
`invertibleOfMulInvertible` 📖	CompOp	1 math math: `Invertible.mulRight_symm_apply`
`invertibleOfPowEqOne` 📖	CompOp	—
`invertiblePow` 📖	CompOp	—
`unitOfInvertible` 📖	CompOp	2 math math: `val_unitOfInvertible`, `val_inv_unitOfInvertible`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commute_invOf` 📖	mathematical	—	`Commute` `Invertible.invOf`	—	`mul_invOf_self` `invOf_mul_self`
`invOf_pow` 📖	mathematical	—	`Invertible.invOf` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne` `Monoid.toNatPow`	—	`invertible_unique`
`invOf_units` 📖	mathematical	—	`Invertible.invOf` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne` `Units.val` `Units` `Units.instInv`	—	`invOf_eq_right_inv` `Units.mul_inv`
`invertibleEquivOfLeftInverse_apply` 📖	mathematical	`DFunLike.coe`	`Equiv` `Invertible` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne` `EquivLike.toFunLike` `Equiv.instEquivLike` `invertibleEquivOfLeftInverse` `Invertible.ofLeftInverse`	—	—
`invertibleEquivOfLeftInverse_symm_apply` 📖	mathematical	`DFunLike.coe`	`Equiv` `Invertible` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `invertibleEquivOfLeftInverse` `Invertible.map`	—	—
`isUnit_of_invertible` 📖	mathematical	—	`IsUnit`	—	—
`map_invOf` 📖	mathematical	—	`DFunLike.coe` `Invertible.invOf` `MulOne.toMul` `MulOneClass.toMulOne` `MulOne.toOne` `Monoid.toMulOneClass`	—	`Invertible.subsingleton`
`nonempty_invertible_iff_isUnit` 📖	mathematical	—	`Invertible` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne` `IsUnit`	—	`isUnit_of_invertible` `IsUnit.nonempty_invertible`
`val_inv_unitOfInvertible` 📖	mathematical	—	`Units.val` `Units` `Units.instInv` `unitOfInvertible` `Invertible.invOf` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	—
`val_unitOfInvertible` 📖	mathematical	—	`Units.val` `unitOfInvertible`	—	—

---

← Back to Index