Documentation Verification Report

Shrink

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

Statistics

Metric	Count
Definitions `algEquiv`, `instAlgebra`	2
Theorems `algEquiv_apply`, `algEquiv_symm_apply`	2
Total	4

Shrink

Definitions

Name	Category	Theorems
`algEquiv` 📖	CompOp	2 math math: `algEquiv_apply`, `algEquiv_symm_apply`
`instAlgebra` 📖	CompOp	2 math math: `algEquiv_apply`, `algEquiv_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Shrink` `instSemiring` `instAlgebra` `AlgEquiv.instFunLike` `algEquiv` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivShrink`	—	—
`algEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Shrink` `instSemiring` `instAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `algEquiv` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivShrink`	—	—

---

← Back to Index