Documentation Verification Report

Shrink

📁 Source: Mathlib/Algebra/Module/Shrink.lean

Statistics

Metric	Count
Definitions `instModule`, `linearEquiv`	2
Theorems `linearEquiv_apply`, `linearEquiv_symm_apply`	2
Total	4

Shrink

Definitions

Name	Category	Theorems
`instModule` 📖	CompOp	9 math math: `linearEquiv_symm_apply`, `Module.Free.Module.free_shrink`, `Module.Flat.shrink`, `continuousLinearEquiv_symm_apply`, `continuousLinearEquiv_apply`, `instFreeCarrierX₂ModuleCatProjectiveShortComplex`, `Module.Finite.Module.finite_shrink`, `linearEquiv_apply`, `ModuleCat.isSeparator`
`linearEquiv` 📖	CompOp	2 math math: `linearEquiv_symm_apply`, `linearEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`linearEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Shrink` `instAddCommMonoid` `instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `linearEquiv` `Equiv` `Equiv.instEquivLike` `Equiv.symm` `equivShrink`	—	`RingHomInvPair.ids`
`linearEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Shrink` `instAddCommMonoid` `instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `linearEquiv` `Equiv` `Equiv.instEquivLike` `equivShrink`	—	`RingHomInvPair.ids`

---

← Back to Index