Documentation Verification Report

TransferInstance

📁 Source: Mathlib/Topology/Algebra/Module/TransferInstance.lean

Statistics

Metric	Count
Definitions `continuousLinearEquiv`, `continuousLinearEquiv`	2
Theorems `toLinearEquiv_continuousLinearEquiv`, `continuousLinearEquiv_apply`, `continuousLinearEquiv_symm_apply`	3
Total	5

Equiv

Definitions

Name	Category	Theorems
`continuousLinearEquiv` 📖	CompOp	1 math math: `toLinearEquiv_continuousLinearEquiv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toLinearEquiv_continuousLinearEquiv` 📖	mathematical	—	`ContinuousLinearEquiv.toLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `topologicalSpace` `addCommMonoid` `module` `continuousLinearEquiv` `linearEquiv`	—	`RingHomInvPair.ids`

Shrink

Definitions

Name	Category	Theorems
`continuousLinearEquiv` 📖	CompOp	2 math math: `continuousLinearEquiv_symm_apply`, `continuousLinearEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousLinearEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Shrink` `instTopologicalSpace` `instAddCommMonoid` `instModule` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `continuousLinearEquiv` `Equiv` `Equiv.instEquivLike` `Equiv.symm` `equivShrink`	—	`RingHomInvPair.ids`
`continuousLinearEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Shrink` `instTopologicalSpace` `instAddCommMonoid` `instModule` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `ContinuousLinearEquiv.symm` `continuousLinearEquiv` `Equiv` `Equiv.instEquivLike` `equivShrink`	—	`RingHomInvPair.ids`

---

← Back to Index