Documentation Verification Report

Unique

📁 Source: Mathlib/LinearAlgebra/Matrix/Unique.lean

Statistics

Metric	Count
Definitions `uniqueAddEquiv`, `uniqueAlgEquiv`, `uniqueEquiv`, `uniqueLinearEquiv`, `uniqueRingEquiv`	5
Theorems `uniqueAddEquiv_apply`, `uniqueAddEquiv_symm_apply`, `uniqueAlgEquiv_apply`, `uniqueAlgEquiv_symm_apply`, `uniqueEquiv_apply`, `uniqueEquiv_symm_apply`, `uniqueLinearEquiv_apply`, `uniqueLinearEquiv_symm_apply`, `uniqueRingEquiv_apply`, `uniqueRingEquiv_symm_apply`	10
Total	15

Matrix

Definitions

Name	Category	Theorems
`uniqueAddEquiv` 📖	CompOp	4 math math: `uniqueAddEquiv_apply`, `uniqueAddEquiv_symm_apply`, `uniqueLinearEquiv_apply`, `uniqueLinearEquiv_symm_apply`
`uniqueAlgEquiv` 📖	CompOp	2 math math: `uniqueAlgEquiv_apply`, `uniqueAlgEquiv_symm_apply`
`uniqueEquiv` 📖	CompOp	2 math math: `uniqueEquiv_symm_apply`, `uniqueEquiv_apply`
`uniqueLinearEquiv` 📖	CompOp	2 math math: `uniqueLinearEquiv_apply`, `uniqueLinearEquiv_symm_apply`
`uniqueRingEquiv` 📖	CompOp	2 math math: `uniqueRingEquiv_apply`, `uniqueRingEquiv_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`uniqueAddEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Matrix` `add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `uniqueAddEquiv` `Unique.instInhabited`	—	—
`uniqueAddEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Matrix` `add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `uniqueAddEquiv` `Equiv` `Equiv.instEquivLike` `of`	—	—
`uniqueAlgEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Matrix` `semiring` `Unique.fintype` `decidableEq_of_subsingleton` `Unique.instSubsingleton` `instAlgebra` `AlgEquiv.instFunLike` `uniqueAlgEquiv` `Unique.instInhabited`	—	`Unique.instSubsingleton`
`uniqueAlgEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Matrix` `semiring` `Unique.fintype` `decidableEq_of_subsingleton` `Unique.instSubsingleton` `instAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `uniqueAlgEquiv` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `of`	—	`Unique.instSubsingleton`
`uniqueEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `uniqueEquiv` `Unique.instInhabited`	—	—
`uniqueEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `uniqueEquiv` `of`	—	—
`uniqueLinearEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Matrix` `addCommMonoid` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `uniqueLinearEquiv` `Equiv.toFun` `AddEquiv.toEquiv` `add` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddCommMonoid.toAddMonoid` `uniqueAddEquiv`	—	`RingHomInvPair.ids`
`uniqueLinearEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Matrix` `addCommMonoid` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `uniqueLinearEquiv` `Equiv.invFun` `AddEquiv.toEquiv` `add` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddCommMonoid.toAddMonoid` `uniqueAddEquiv`	—	`RingHomInvPair.ids`
`uniqueRingEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `Matrix` `instMulOfFintypeOfAddCommMonoid` `Unique.fintype` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid` `add` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `uniqueRingEquiv` `Unique.instInhabited`	—	—
`uniqueRingEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `Matrix` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `instMulOfFintypeOfAddCommMonoid` `Unique.fintype` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Distrib.toAdd` `add` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `uniqueRingEquiv` `Equiv` `Equiv.instEquivLike` `of`	—	—

---

← Back to Index